| Step | Hyp | Ref
| Expression |
| 1 | | imassrn 6089 |
. . . 4
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 |
| 2 | | qustgp.h |
. . . . . . 7
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) |
| 3 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))) |
| 4 | | qustgpopn.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐺) |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑋 = (Base‘𝐺)) |
| 6 | | qustgpopn.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) |
| 7 | | ovex 7464 |
. . . . . . 7
⊢ (𝐺 ~QG 𝑌) ∈ V |
| 8 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (𝐺 ~QG 𝑌) ∈ V) |
| 9 | | simp1 1137 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐺 ∈ TopGrp) |
| 10 | 3, 5, 6, 8, 9 | quslem 17588 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) |
| 11 | | forn 6823 |
. . . . 5
⊢ (𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌)) → ran 𝐹 = (𝑋 / (𝐺 ~QG 𝑌))) |
| 12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → ran 𝐹 = (𝑋 / (𝐺 ~QG 𝑌))) |
| 13 | 1, 12 | sseqtrid 4026 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (𝐹 “ 𝑆) ⊆ (𝑋 / (𝐺 ~QG 𝑌))) |
| 14 | | eceq1 8784 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → [𝑥](𝐺 ~QG 𝑌) = [𝑦](𝐺 ~QG 𝑌)) |
| 15 | 14 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) = (𝑦 ∈ 𝑋 ↦ [𝑦](𝐺 ~QG 𝑌)) |
| 16 | 6, 15 | eqtri 2765 |
. . . . . . . 8
⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ [𝑦](𝐺 ~QG 𝑌)) |
| 17 | 16 | mptpreima 6258 |
. . . . . . 7
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) = {𝑦 ∈ 𝑋 ∣ [𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆)} |
| 18 | 17 | reqabi 3460 |
. . . . . 6
⊢ (𝑦 ∈ (◡𝐹 “ (𝐹 “ 𝑆)) ↔ (𝑦 ∈ 𝑋 ∧ [𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆))) |
| 19 | 6 | funmpt2 6605 |
. . . . . . . . 9
⊢ Fun 𝐹 |
| 20 | | fvelima 6974 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ [𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆)) → ∃𝑧 ∈ 𝑆 (𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌)) |
| 21 | 19, 20 | mpan 690 |
. . . . . . . 8
⊢ ([𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆) → ∃𝑧 ∈ 𝑆 (𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌)) |
| 22 | | qustgpopn.j |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 = (TopOpen‘𝐺) |
| 23 | 22, 4 | tgptopon 24090 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
| 24 | 9, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝑋)) |
| 25 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ 𝐽) |
| 26 | | toponss 22933 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ 𝐽) → 𝑆 ⊆ 𝑋) |
| 27 | 24, 25, 26 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ⊆ 𝑋) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
| 29 | 28 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑋) |
| 30 | | eceq1 8784 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → [𝑥](𝐺 ~QG 𝑌) = [𝑧](𝐺 ~QG 𝑌)) |
| 31 | | ecexg 8749 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑧](𝐺 ~QG 𝑌) ∈ V) |
| 32 | 7, 31 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ [𝑧](𝐺 ~QG 𝑌) ∈ V |
| 33 | 30, 6, 32 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑋 → (𝐹‘𝑧) = [𝑧](𝐺 ~QG 𝑌)) |
| 34 | 29, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) = [𝑧](𝐺 ~QG 𝑌)) |
| 35 | 34 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌) ↔ [𝑧](𝐺 ~QG 𝑌) = [𝑦](𝐺 ~QG 𝑌))) |
| 36 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ ([𝑧](𝐺 ~QG 𝑌) = [𝑦](𝐺 ~QG 𝑌) ↔ [𝑦](𝐺 ~QG 𝑌) = [𝑧](𝐺 ~QG 𝑌)) |
| 37 | 35, 36 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌) ↔ [𝑦](𝐺 ~QG 𝑌) = [𝑧](𝐺 ~QG 𝑌))) |
| 38 | | nsgsubg 19176 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝑌 ∈ (SubGrp‘𝐺)) |
| 39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑌 ∈ (SubGrp‘𝐺)) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝑌 ∈ (SubGrp‘𝐺)) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ~QG 𝑌) = (𝐺 ~QG 𝑌) |
| 42 | 4, 41 | eqger 19196 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑌) Er 𝑋) |
| 43 | 40, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → (𝐺 ~QG 𝑌) Er 𝑋) |
| 44 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝑋) |
| 45 | 43, 44 | erth 8796 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → (𝑦(𝐺 ~QG 𝑌)𝑧 ↔ [𝑦](𝐺 ~QG 𝑌) = [𝑧](𝐺 ~QG 𝑌))) |
| 46 | 9 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝐺 ∈ TopGrp) |
| 47 | 4 | subgss 19145 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
| 48 | 40, 47 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝑌 ⊆ 𝑋) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 50 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 51 | 4, 49, 50, 41 | eqgval 19195 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ⊆ 𝑋) → (𝑦(𝐺 ~QG 𝑌)𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌))) |
| 52 | 46, 48, 51 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → (𝑦(𝐺 ~QG 𝑌)𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌))) |
| 53 | 37, 45, 52 | 3bitr2d 307 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌) ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌))) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
| 56 | 50, 54, 55 | oppgplus 19367 |
. . . . . . . . . . . . . . . . 17
⊢
((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎) = (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) |
| 57 | 56 | mpteq2i 5247 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑋 ↦ ((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎)) = (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 58 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝐺 ∈ TopGrp) |
| 59 | 54 | oppgtgp 24106 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ TopGrp →
(oppg‘𝐺) ∈ TopGrp) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (oppg‘𝐺) ∈
TopGrp) |
| 61 | 48 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝑋 ↦ ((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎)) = (𝑎 ∈ 𝑋 ↦ ((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎)) |
| 63 | 54, 4 | oppgbas 19370 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 =
(Base‘(oppg‘𝐺)) |
| 64 | 54, 22 | oppgtopn 19372 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐽 =
(TopOpen‘(oppg‘𝐺)) |
| 65 | 62, 63, 55, 64 | tgplacthmeo 24111 |
. . . . . . . . . . . . . . . . 17
⊢
(((oppg‘𝐺) ∈ TopGrp ∧
(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) → (𝑎 ∈ 𝑋 ↦ ((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎)) ∈ (𝐽Homeo𝐽)) |
| 66 | 60, 61, 65 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑎 ∈ 𝑋 ↦ ((((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)(+g‘(oppg‘𝐺))𝑎)) ∈ (𝐽Homeo𝐽)) |
| 67 | 57, 66 | eqeltrrid 2846 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐽Homeo𝐽)) |
| 68 | | hmeocn 23768 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐽Homeo𝐽) → (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐽 Cn 𝐽)) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐽 Cn 𝐽)) |
| 70 | 25 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝑆 ∈ 𝐽) |
| 71 | | cnima 23273 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐽 Cn 𝐽) ∧ 𝑆 ∈ 𝐽) → (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ∈ 𝐽) |
| 72 | 69, 70, 71 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ∈ 𝐽) |
| 73 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝑦 ∈ 𝑋) |
| 74 | | tgpgrp 24086 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
| 75 | 58, 74 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝐺 ∈ Grp) |
| 76 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 77 | 4, 50, 76, 49 | grprinv 19008 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
| 78 | 75, 73, 77 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
| 79 | 78 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = ((0g‘𝐺)(+g‘𝐺)𝑧)) |
| 80 | 4, 49 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
| 81 | 75, 73, 80 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
| 82 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝑧 ∈ 𝑋) |
| 83 | 4, 50 | grpass 18960 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 84 | 75, 73, 81, 82, 83 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 85 | 4, 50, 76 | grplid 18985 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)𝑧) = 𝑧) |
| 86 | 75, 82, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ((0g‘𝐺)(+g‘𝐺)𝑧) = 𝑧) |
| 87 | 79, 84, 86 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = 𝑧) |
| 88 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝑧 ∈ 𝑆) |
| 89 | 87, 88 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆) |
| 90 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑦 → (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 91 | 90 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → ((𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆 ↔ (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆)) |
| 92 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = (𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 93 | 92 | mptpreima 6258 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) = {𝑎 ∈ 𝑋 ∣ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆} |
| 94 | 91, 93 | elrab2 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ↔ (𝑦 ∈ 𝑋 ∧ (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆)) |
| 95 | 73, 89, 94 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → 𝑦 ∈ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆)) |
| 96 | | ecexg 8749 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V) |
| 97 | 7, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ [𝑥](𝐺 ~QG 𝑌) ∈ V |
| 98 | 97, 6 | fnmpti 6711 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐹 Fn 𝑋 |
| 99 | 28 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
| 100 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝑋 ∧ 𝑆 ⊆ 𝑋 ∧ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆) → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐹 “ 𝑆)) |
| 101 | 100 | 3expia 1122 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝑋 ∧ 𝑆 ⊆ 𝑋) → ((𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆 → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐹 “ 𝑆))) |
| 102 | 98, 99, 101 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆 → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐹 “ 𝑆))) |
| 103 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 104 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ 𝑋) |
| 105 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) |
| 106 | 4, 50 | grpcl 18959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) → (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑋) |
| 107 | 103, 104,
105, 106 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑋) |
| 108 | | eceq1 8784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) → [𝑥](𝐺 ~QG 𝑌) = [(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))](𝐺 ~QG 𝑌)) |
| 109 | 108, 6, 97 | fvmpt3i 7021 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑋 → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = [(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))](𝐺 ~QG 𝑌)) |
| 110 | 107, 109 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = [(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))](𝐺 ~QG 𝑌)) |
| 111 | 43 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (𝐺 ~QG 𝑌) Er 𝑋) |
| 112 | 4, 50, 76, 49 | grplinv 19007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑎)(+g‘𝐺)𝑎) = (0g‘𝐺)) |
| 113 | 103, 104,
112 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑎)(+g‘𝐺)𝑎) = (0g‘𝐺)) |
| 114 | 113 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((((invg‘𝐺)‘𝑎)(+g‘𝐺)𝑎)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = ((0g‘𝐺)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 115 | 4, 49 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋) → ((invg‘𝐺)‘𝑎) ∈ 𝑋) |
| 116 | 103, 104,
115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((invg‘𝐺)‘𝑎) ∈ 𝑋) |
| 117 | 4, 50 | grpass 18960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑎) ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋)) → ((((invg‘𝐺)‘𝑎)(+g‘𝐺)𝑎)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)))) |
| 118 | 103, 116,
104, 105, 117 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((((invg‘𝐺)‘𝑎)(+g‘𝐺)𝑎)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)))) |
| 119 | 4, 50, 76 | grplid 18985 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) |
| 120 | 103, 105,
119 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) |
| 121 | 114, 118,
120 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) |
| 122 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) |
| 123 | 121, 122 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ 𝑌) |
| 124 | 48 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → 𝑌 ⊆ 𝑋) |
| 125 | 4, 49, 50, 41 | eqgval 19195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑎(𝐺 ~QG 𝑌)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ↔ (𝑎 ∈ 𝑋 ∧ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ 𝑌))) |
| 126 | 103, 124,
125 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (𝑎(𝐺 ~QG 𝑌)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ↔ (𝑎 ∈ 𝑋 ∧ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑎)(+g‘𝐺)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ 𝑌))) |
| 127 | 104, 107,
123, 126 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → 𝑎(𝐺 ~QG 𝑌)(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
| 128 | 111, 127 | erthi 8798 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → [𝑎](𝐺 ~QG 𝑌) = [(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))](𝐺 ~QG 𝑌)) |
| 129 | 110, 128 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → (𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = [𝑎](𝐺 ~QG 𝑌)) |
| 130 | 129 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((𝐹‘(𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) ∈ (𝐹 “ 𝑆) ↔ [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆))) |
| 131 | 102, 130 | sylibd 239 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) ∧ 𝑎 ∈ 𝑋) → ((𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆 → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆))) |
| 132 | 131 | ss2rabdv 4076 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → {𝑎 ∈ 𝑋 ∣ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑆} ⊆ {𝑎 ∈ 𝑋 ∣ [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆)}) |
| 133 | | eceq1 8784 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌)) |
| 134 | 133 | cbvmptv 5255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) = (𝑎 ∈ 𝑋 ↦ [𝑎](𝐺 ~QG 𝑌)) |
| 135 | 6, 134 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑎 ∈ 𝑋 ↦ [𝑎](𝐺 ~QG 𝑌)) |
| 136 | 135 | mptpreima 6258 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) = {𝑎 ∈ 𝑋 ∣ [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆)} |
| 137 | 132, 93, 136 | 3sstr4g 4037 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) |
| 138 | | eleq2 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) → (𝑦 ∈ 𝑢 ↔ 𝑦 ∈ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆))) |
| 139 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) → (𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)) ↔ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) |
| 140 | 138, 139 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) ↔ (𝑦 ∈ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ∧ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 141 | 140 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ (((◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ∈ 𝐽 ∧ (𝑦 ∈ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ∧ (◡(𝑎 ∈ 𝑋 ↦ (𝑎(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) “ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) |
| 142 | 72, 95, 137, 141 | syl12anc 837 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) |
| 143 | 142 | 3ad2antr3 1191 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺) ∧
𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌)) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) |
| 144 | 143 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 145 | 53, 144 | sylbid 240 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 146 | 145 | rexlimdva 3155 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ 𝑆 (𝐹‘𝑧) = [𝑦](𝐺 ~QG 𝑌) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 147 | 21, 146 | syl5 34 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) ∧ 𝑦 ∈ 𝑋) → ([𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 148 | 147 | expimpd 453 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → ((𝑦 ∈ 𝑋 ∧ [𝑦](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑆)) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 149 | 18, 148 | biimtrid 242 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (𝑦 ∈ (◡𝐹 “ (𝐹 “ 𝑆)) → ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 150 | 149 | ralrimiv 3145 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → ∀𝑦 ∈ (◡𝐹 “ (𝐹 “ 𝑆))∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))) |
| 151 | | topontop 22919 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 152 | | eltop2 22982 |
. . . . 5
⊢ (𝐽 ∈ Top → ((◡𝐹 “ (𝐹 “ 𝑆)) ∈ 𝐽 ↔ ∀𝑦 ∈ (◡𝐹 “ (𝐹 “ 𝑆))∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 153 | 24, 151, 152 | 3syl 18 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → ((◡𝐹 “ (𝐹 “ 𝑆)) ∈ 𝐽 ↔ ∀𝑦 ∈ (◡𝐹 “ (𝐹 “ 𝑆))∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))))) |
| 154 | 150, 153 | mpbird 257 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑆)) ∈ 𝐽) |
| 155 | | elqtop3 23711 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) → ((𝐹 “ 𝑆) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑆) ⊆ (𝑋 / (𝐺 ~QG 𝑌)) ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ∈ 𝐽))) |
| 156 | 24, 10, 155 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → ((𝐹 “ 𝑆) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑆) ⊆ (𝑋 / (𝐺 ~QG 𝑌)) ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ∈ 𝐽))) |
| 157 | 13, 154, 156 | mpbir2and 713 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (𝐹 “ 𝑆) ∈ (𝐽 qTop 𝐹)) |
| 158 | 3, 5, 6, 8, 9 | qusval 17587 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐻 = (𝐹 “s 𝐺)) |
| 159 | | qustgpopn.k |
. . 3
⊢ 𝐾 = (TopOpen‘𝐻) |
| 160 | 158, 5, 10, 9, 22, 159 | imastopn 23728 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝐾 = (𝐽 qTop 𝐹)) |
| 161 | 157, 160 | eleqtrrd 2844 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → (𝐹 “ 𝑆) ∈ 𝐾) |