| Step | Hyp | Ref
| Expression |
| 1 | | qusker.n |
. . . . 5
⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺))) |
| 3 | | qusker.b |
. . . . 5
⊢ 𝑉 = (Base‘𝑀) |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝑉 = (Base‘𝑀)) |
| 5 | | qusker.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) |
| 6 | | ovex 7464 |
. . . . 5
⊢ (𝑀 ~QG 𝐺) ∈ V |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (𝑀 ~QG 𝐺) ∈ V) |
| 8 | | nsgsubg 19176 |
. . . . 5
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝐺 ∈ (SubGrp‘𝑀)) |
| 9 | | subgrcl 19149 |
. . . . 5
⊢ (𝐺 ∈ (SubGrp‘𝑀) → 𝑀 ∈ Grp) |
| 10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝑀 ∈ Grp) |
| 11 | 2, 4, 5, 7, 10 | quslem 17588 |
. . 3
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝐹:𝑉–onto→(𝑉 / (𝑀 ~QG 𝐺))) |
| 12 | | fofn 6822 |
. . 3
⊢ (𝐹:𝑉–onto→(𝑉 / (𝑀 ~QG 𝐺)) → 𝐹 Fn 𝑉) |
| 13 | | fniniseg2 7082 |
. . 3
⊢ (𝐹 Fn 𝑉 → (◡𝐹 “ { 0 }) = {𝑦 ∈ 𝑉 ∣ (𝐹‘𝑦) = 0 }) |
| 14 | 11, 12, 13 | 3syl 18 |
. 2
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = {𝑦 ∈ 𝑉 ∣ (𝐹‘𝑦) = 0 }) |
| 15 | | qusker.1 |
. . . . . 6
⊢ 0 =
(0g‘𝑁) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 17 | 1, 16 | qus0 19207 |
. . . . . 6
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) →
[(0g‘𝑀)](𝑀 ~QG 𝐺) = (0g‘𝑁)) |
| 18 | 15, 17 | eqtr4id 2796 |
. . . . 5
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 0 =
[(0g‘𝑀)](𝑀 ~QG 𝐺)) |
| 19 | | eceq1 8784 |
. . . . . 6
⊢ (𝑥 = 𝑦 → [𝑥](𝑀 ~QG 𝐺) = [𝑦](𝑀 ~QG 𝐺)) |
| 20 | | ecexg 8749 |
. . . . . . 7
⊢ ((𝑀 ~QG 𝐺) ∈ V → [𝑦](𝑀 ~QG 𝐺) ∈ V) |
| 21 | 6, 20 | ax-mp 5 |
. . . . . 6
⊢ [𝑦](𝑀 ~QG 𝐺) ∈ V |
| 22 | 19, 5, 21 | fvmpt 7016 |
. . . . 5
⊢ (𝑦 ∈ 𝑉 → (𝐹‘𝑦) = [𝑦](𝑀 ~QG 𝐺)) |
| 23 | 18, 22 | eqeqan12d 2751 |
. . . 4
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ( 0 = (𝐹‘𝑦) ↔ [(0g‘𝑀)](𝑀 ~QG 𝐺) = [𝑦](𝑀 ~QG 𝐺))) |
| 24 | | eqcom 2744 |
. . . . 5
⊢ ( 0 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 0 ) |
| 25 | 24 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ( 0 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 0 )) |
| 26 | | simpl 482 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → 𝐺 ∈ (NrmSGrp‘𝑀)) |
| 27 | | simpr 484 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
| 28 | 3, 16 | grpidcl 18983 |
. . . . . . 7
⊢ (𝑀 ∈ Grp →
(0g‘𝑀)
∈ 𝑉) |
| 29 | 26, 10, 28 | 3syl 18 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → (0g‘𝑀) ∈ 𝑉) |
| 30 | 3 | subgss 19145 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (SubGrp‘𝑀) → 𝐺 ⊆ 𝑉) |
| 31 | 8, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → 𝐺 ⊆ 𝑉) |
| 32 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝑀) = (invg‘𝑀) |
| 33 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 34 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑀 ~QG 𝐺) = (𝑀 ~QG 𝐺) |
| 35 | 3, 32, 33, 34 | eqgval 19195 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Grp ∧ 𝐺 ⊆ 𝑉) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺))) |
| 36 | 10, 31, 35 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) →
((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺))) |
| 37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺))) |
| 38 | | df-3an 1089 |
. . . . . . . . 9
⊢
(((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺) ↔ (((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺)) |
| 39 | 38 | biancomi 462 |
. . . . . . . 8
⊢
(((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺) ↔ ((((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺 ∧ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 40 | 37, 39 | bitrdi 287 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ ((((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺 ∧ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))) |
| 41 | 40 | rbaibd 540 |
. . . . . 6
⊢ (((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) ∧ ((0g‘𝑀) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺)) |
| 42 | 26, 27, 29, 27, 41 | syl22anc 839 |
. . . . 5
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺)) |
| 43 | 3, 34 | eqger 19196 |
. . . . . . . 8
⊢ (𝐺 ∈ (SubGrp‘𝑀) → (𝑀 ~QG 𝐺) Er 𝑉) |
| 44 | 8, 43 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (𝑀 ~QG 𝐺) Er 𝑉) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → (𝑀 ~QG 𝐺) Er 𝑉) |
| 46 | 45, 27 | erth2 8797 |
. . . . 5
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(𝑀 ~QG 𝐺)𝑦 ↔ [(0g‘𝑀)](𝑀 ~QG 𝐺) = [𝑦](𝑀 ~QG 𝐺))) |
| 47 | 16, 32 | grpinvid 19017 |
. . . . . . . . 9
⊢ (𝑀 ∈ Grp →
((invg‘𝑀)‘(0g‘𝑀)) = (0g‘𝑀)) |
| 48 | 26, 10, 47 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((invg‘𝑀)‘(0g‘𝑀)) = (0g‘𝑀)) |
| 49 | 48 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) = ((0g‘𝑀)(+g‘𝑀)𝑦)) |
| 50 | 3, 33, 16 | grplid 18985 |
. . . . . . . 8
⊢ ((𝑀 ∈ Grp ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(+g‘𝑀)𝑦) = 𝑦) |
| 51 | 10, 50 | sylan 580 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((0g‘𝑀)(+g‘𝑀)𝑦) = 𝑦) |
| 52 | 49, 51 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → (((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) = 𝑦) |
| 53 | 52 | eleq1d 2826 |
. . . . 5
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((((invg‘𝑀)‘(0g‘𝑀))(+g‘𝑀)𝑦) ∈ 𝐺 ↔ 𝑦 ∈ 𝐺)) |
| 54 | 42, 46, 53 | 3bitr3d 309 |
. . . 4
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ([(0g‘𝑀)](𝑀 ~QG 𝐺) = [𝑦](𝑀 ~QG 𝐺) ↔ 𝑦 ∈ 𝐺)) |
| 55 | 23, 25, 54 | 3bitr3d 309 |
. . 3
⊢ ((𝐺 ∈ (NrmSGrp‘𝑀) ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑦) = 0 ↔ 𝑦 ∈ 𝐺)) |
| 56 | 55 | rabbidva 3443 |
. 2
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → {𝑦 ∈ 𝑉 ∣ (𝐹‘𝑦) = 0 } = {𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺}) |
| 57 | | dfss7 4251 |
. . 3
⊢ (𝐺 ⊆ 𝑉 ↔ {𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺} = 𝐺) |
| 58 | 31, 57 | sylib 218 |
. 2
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → {𝑦 ∈ 𝑉 ∣ 𝑦 ∈ 𝐺} = 𝐺) |
| 59 | 14, 56, 58 | 3eqtrd 2781 |
1
⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) |