Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. 2
⊢ (𝑋 / ∼ ) = (𝑋 / ∼ ) |
2 | | breq2 4006 |
. 2
⊢ ([𝑥] ∼ = 𝐴 → (𝑌 ≈ [𝑥] ∼ ↔ 𝑌 ≈ 𝐴)) |
3 | | simpl 109 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ (SubGrp‘𝐺)) |
4 | | subgrcl 12970 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | | eqger.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
6 | 5 | subgss 12965 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
7 | 4, 6 | jca 306 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋)) |
8 | | eqger.r |
. . . . . . . 8
⊢ ∼ =
(𝐺 ~QG
𝑌) |
9 | | eqid 2177 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
10 | 5, 8, 9 | eqglact 13015 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
11 | 10 | 3expa 1203 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
12 | 7, 11 | sylan 283 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
13 | 5, 8 | eqger 13014 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
14 | | basfn 12512 |
. . . . . . . . . 10
⊢ Base Fn
V |
15 | 4 | elexd 2750 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ V) |
16 | | funfvex 5531 |
. . . . . . . . . . 11
⊢ ((Fun
Base ∧ 𝐺 ∈ dom
Base) → (Base‘𝐺)
∈ V) |
17 | 16 | funfni 5315 |
. . . . . . . . . 10
⊢ ((Base Fn
V ∧ 𝐺 ∈ V) →
(Base‘𝐺) ∈
V) |
18 | 14, 15, 17 | sylancr 414 |
. . . . . . . . 9
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (Base‘𝐺) ∈ V) |
19 | 5, 18 | eqeltrid 2264 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑋 ∈ V) |
20 | | erex 6556 |
. . . . . . . 8
⊢ ( ∼ Er
𝑋 → (𝑋 ∈ V → ∼ ∈
V)) |
21 | 13, 19, 20 | sylc 62 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ ∈
V) |
22 | | ecexg 6536 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝑥] ∼ ∈
V) |
23 | 21, 22 | syl 14 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → [𝑥] ∼ ∈
V) |
24 | 23 | adantr 276 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → [𝑥] ∼ ∈
V) |
25 | 12, 24 | eqeltrrd 2255 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌) ∈ V) |
26 | | eqid 2177 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧))) = (𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧))) |
27 | 26, 5, 9 | grplactf1o 12905 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥):𝑋–1-1-onto→𝑋) |
28 | 26, 5 | grplactfval 12903 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥) = (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧))) |
29 | 28 | adantl 277 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥) = (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧))) |
30 | 29 | f1oeq1d 5455 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (((𝑦 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)))‘𝑥):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)) |
31 | 27, 30 | mpbid 147 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
32 | 4, 31 | sylan 283 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
33 | | f1of1 5459 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋) |
34 | 32, 33 | syl 14 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋) |
35 | 6 | adantr 276 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ⊆ 𝑋) |
36 | | f1ores 5475 |
. . . . 5
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)):𝑋–1-1→𝑋 ∧ 𝑌 ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
37 | 34, 35, 36 | syl2anc 411 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
38 | | f1oen2g 6752 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌) ∈ V ∧ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) ↾ 𝑌):𝑌–1-1-onto→((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) → 𝑌 ≈ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
39 | 3, 25, 37, 38 | syl3anc 1238 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ≈ ((𝑧 ∈ 𝑋 ↦ (𝑥(+g‘𝐺)𝑧)) “ 𝑌)) |
40 | 39, 12 | breqtrrd 4030 |
. 2
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑌 ≈ [𝑥] ∼ ) |
41 | 1, 2, 40 | ectocld 6598 |
1
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝐴) |