| Step | Hyp | Ref
| Expression |
| 1 | | qusgrp.h |
. . . 4
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))) |
| 3 | | eqidd 2738 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → (Base‘𝐺) = (Base‘𝐺)) |
| 4 | | eqidd 2738 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) →
(+g‘𝐺) =
(+g‘𝐺)) |
| 5 | | nsgsubg 19176 |
. . . 4
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 7 | | eqid 2737 |
. . . . 5
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
| 8 | 6, 7 | eqger 19196 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑆) Er (Base‘𝐺)) |
| 9 | 5, 8 | syl 17 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → (𝐺 ~QG 𝑆) Er (Base‘𝐺)) |
| 10 | | subgrcl 19149 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 11 | 5, 10 | syl 17 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ Grp) |
| 12 | | eqid 2737 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 13 | 6, 7, 12 | eqgcpbl 19200 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → ((𝑎(𝐺 ~QG 𝑆)𝑐 ∧ 𝑏(𝐺 ~QG 𝑆)𝑑) → (𝑎(+g‘𝐺)𝑏)(𝐺 ~QG 𝑆)(𝑐(+g‘𝐺)𝑑))) |
| 14 | 6, 12 | grpcl 18959 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺)) → (𝑢(+g‘𝐺)𝑣) ∈ (Base‘𝐺)) |
| 15 | 11, 14 | syl3an1 1164 |
. . 3
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺)) → (𝑢(+g‘𝐺)𝑣) ∈ (Base‘𝐺)) |
| 16 | 9 | adantr 480 |
. . . . 5
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → (𝐺 ~QG 𝑆) Er (Base‘𝐺)) |
| 17 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp) |
| 18 | | simpr1 1195 |
. . . . . . 7
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → 𝑢 ∈ (Base‘𝐺)) |
| 19 | | simpr2 1196 |
. . . . . . 7
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → 𝑣 ∈ (Base‘𝐺)) |
| 20 | 17, 18, 19, 14 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → (𝑢(+g‘𝐺)𝑣) ∈ (Base‘𝐺)) |
| 21 | | simpr3 1197 |
. . . . . 6
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → 𝑤 ∈ (Base‘𝐺)) |
| 22 | 6, 12 | grpcl 18959 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑢(+g‘𝐺)𝑣) ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺)) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤) ∈ (Base‘𝐺)) |
| 23 | 17, 20, 21, 22 | syl3anc 1373 |
. . . . 5
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤) ∈ (Base‘𝐺)) |
| 24 | 16, 23 | erref 8765 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤)(𝐺 ~QG 𝑆)((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤)) |
| 25 | 6, 12 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤) = (𝑢(+g‘𝐺)(𝑣(+g‘𝐺)𝑤))) |
| 26 | 11, 25 | sylan 580 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤) = (𝑢(+g‘𝐺)(𝑣(+g‘𝐺)𝑤))) |
| 27 | 24, 26 | breqtrd 5169 |
. . 3
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺) ∧ 𝑤 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)𝑣)(+g‘𝐺)𝑤)(𝐺 ~QG 𝑆)(𝑢(+g‘𝐺)(𝑣(+g‘𝐺)𝑤))) |
| 28 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 29 | 6, 28 | grpidcl 18983 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 30 | 11, 29 | syl 17 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 31 | 6, 12, 28 | grplid 18985 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) →
((0g‘𝐺)(+g‘𝐺)𝑢) = 𝑢) |
| 32 | 11, 31 | sylan 580 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → ((0g‘𝐺)(+g‘𝐺)𝑢) = 𝑢) |
| 33 | 9 | adantr 480 |
. . . . 5
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (𝐺 ~QG 𝑆) Er (Base‘𝐺)) |
| 34 | | simpr 484 |
. . . . 5
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → 𝑢 ∈ (Base‘𝐺)) |
| 35 | 33, 34 | erref 8765 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → 𝑢(𝐺 ~QG 𝑆)𝑢) |
| 36 | 32, 35 | eqbrtrd 5165 |
. . 3
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → ((0g‘𝐺)(+g‘𝐺)𝑢)(𝐺 ~QG 𝑆)𝑢) |
| 37 | | eqid 2737 |
. . . . 5
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 38 | 6, 37 | grpinvcl 19005 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑢) ∈ (Base‘𝐺)) |
| 39 | 11, 38 | sylan 580 |
. . 3
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑢) ∈ (Base‘𝐺)) |
| 40 | 6, 12, 28, 37 | grplinv 19007 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) →
(((invg‘𝐺)‘𝑢)(+g‘𝐺)𝑢) = (0g‘𝐺)) |
| 41 | 11, 40 | sylan 580 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (((invg‘𝐺)‘𝑢)(+g‘𝐺)𝑢) = (0g‘𝐺)) |
| 42 | 30 | adantr 480 |
. . . . 5
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (0g‘𝐺) ∈ (Base‘𝐺)) |
| 43 | 33, 42 | erref 8765 |
. . . 4
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (0g‘𝐺)(𝐺 ~QG 𝑆)(0g‘𝐺)) |
| 44 | 41, 43 | eqbrtrd 5165 |
. . 3
⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (((invg‘𝐺)‘𝑢)(+g‘𝐺)𝑢)(𝐺 ~QG 𝑆)(0g‘𝐺)) |
| 45 | 2, 3, 4, 9, 11, 13, 15, 27, 30, 36, 39, 44 | qusgrp2 19076 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → (𝐻 ∈ Grp ∧
[(0g‘𝐺)](𝐺 ~QG 𝑆) = (0g‘𝐻))) |
| 46 | 45 | simpld 494 |
1
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) |