Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. 2
⊢ (𝑋 / ∼ ) = (𝑋 / ∼ ) |
2 | | breq2 5078 |
. 2
⊢ ([𝑥] ∼ = 𝐴 → (𝑌 ≈ [𝑥] ∼ ↔ 𝑌 ≈ 𝐴)) |
3 | | simpl 483 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ (SubGrp‘𝐺)) |
4 | | subgrcl 18760 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | | eqger.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
6 | 5 | subgss 18756 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
7 | 4, 6 | jca 512 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋)) |
8 | | eqger.r |
. . . . . . . 8
⊢ ∼ =
(𝐺 ~QG
𝑌) |
9 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
10 | 5, 8, 9 | eqglact 18807 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
11 | 10 | 3expa 1117 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
12 | 7, 11 | sylan 580 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
13 | 8 | ovexi 7309 |
. . . . . 6
⊢ ∼ ∈
V |
14 | | ecexg 8502 |
. . . . . 6
⊢ ( ∼ ∈
V → [𝑥] ∼ ∈
V) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
⊢ [𝑥] ∼ ∈
V |
16 | 12, 15 | eqeltrrdi 2848 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌) ∈ V) |
17 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧))) = (𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧))) |
18 | 17, 5, 9 | grplactf1o 18679 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥):𝑋–1-1-onto→𝑋) |
19 | 17, 5 | grplactfval 18676 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥) = (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧))) |
20 | 19 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥) = (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧))) |
21 | 20 | f1oeq1d 6711 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)) |
22 | 18, 21 | mpbid 231 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
23 | 4, 22 | sylan 580 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
24 | | f1of1 6715 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋) |
26 | 6 | adantr 481 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ⊆ 𝑋) |
27 | | f1ores 6730 |
. . . . 5
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋 ∧ 𝑌 ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
28 | 25, 26, 27 | syl2anc 584 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
29 | | f1oen2g 8756 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌) ∈ V ∧ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) → 𝑌 ≈ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
30 | 3, 16, 28, 29 | syl3anc 1370 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ≈ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
31 | 30, 12 | breqtrrd 5102 |
. 2
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ≈ [𝑥] ∼ ) |
32 | 1, 2, 31 | ectocld 8573 |
1
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝐴) |