| Step | Hyp | Ref
| Expression |
| 1 | | ghmqusker.1 |
. . 3
⊢ 0 =
(0g‘𝐻) |
| 2 | | ghmqusker.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
| 3 | | ghmqusker.k |
. . 3
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
| 4 | | ghmqusker.q |
. . 3
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) |
| 5 | | ghmqusker.j |
. . 3
⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪
(𝐹 “ 𝑞)) |
| 6 | 1, 2, 3, 4, 5 | ghmquskerlem3 19304 |
. 2
⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻)) |
| 7 | | ghmgrp1 19236 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) |
| 8 | 2, 7 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 9 | 8 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐺 ∈ Grp) |
| 10 | 1 | ghmker 19260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (◡𝐹 “ { 0 }) ∈
(NrmSGrp‘𝐺)) |
| 11 | 2, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐹 “ { 0 }) ∈
(NrmSGrp‘𝐺)) |
| 12 | 3, 11 | eqeltrid 2845 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ (NrmSGrp‘𝐺)) |
| 13 | | nsgsubg 19176 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → 𝐾 ∈ (SubGrp‘𝐺)) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
| 15 | 14 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐾 ∈ (SubGrp‘𝐺)) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 18 | 16, 17 | ghmf 19238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) |
| 19 | 2, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) |
| 20 | 19 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn (Base‘𝐺)) |
| 21 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝐹 Fn (Base‘𝐺)) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝐹 Fn (Base‘𝐺)) |
| 23 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))) |
| 24 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺)) |
| 25 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐺 ~QG 𝐾) ∈ V) |
| 26 | 23, 24, 25, 8 | qusbas 17590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄)) |
| 27 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ~QG 𝐾) = (𝐺 ~QG 𝐾) |
| 28 | 16, 27 | eqger 19196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
| 29 | 12, 13, 28 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
| 30 | 29 | qsss 8818 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ⊆ 𝒫 (Base‘𝐺)) |
| 31 | 26, 30 | eqsstrrd 4019 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (Base‘𝑄) ⊆ 𝒫
(Base‘𝐺)) |
| 32 | 31 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ 𝒫 (Base‘𝐺)) |
| 33 | 32 | elpwid 4609 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ⊆ (Base‘𝐺)) |
| 34 | 33 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) → 𝑥 ∈ (Base‘𝐺)) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝑥 ∈ (Base‘𝐺)) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ (Base‘𝐺)) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘𝑟) = (𝐹‘𝑥)) |
| 38 | 37 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ((𝐽‘𝑟) = 0 ↔ (𝐹‘𝑥) = 0 )) |
| 39 | 38 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → (𝐹‘𝑥) = 0 ) |
| 40 | | fniniseg 7080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝐺) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝐹‘𝑥) = 0 ))) |
| 41 | 40 | biimpar 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn (Base‘𝐺) ∧ (𝑥 ∈ (Base‘𝐺) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 })) |
| 42 | 22, 36, 39, 41 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ (◡𝐹 “ { 0 })) |
| 43 | 42, 3 | eleqtrrdi 2852 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ 𝐾) |
| 44 | 27 | eqg0el 19201 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ∈ (SubGrp‘𝐺)) → ([𝑥](𝐺 ~QG 𝐾) = 𝐾 ↔ 𝑥 ∈ 𝐾)) |
| 45 | 44 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝐾 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝐾) → [𝑥](𝐺 ~QG 𝐾) = 𝐾) |
| 46 | 9, 15, 43, 45 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → [𝑥](𝐺 ~QG 𝐾) = 𝐾) |
| 47 | 29 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
| 48 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ (Base‘𝑄)) |
| 49 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄)) |
| 50 | 48, 49 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
| 51 | 50 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
| 52 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑥 ∈ 𝑟) |
| 53 | | qsel 8836 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ~QG 𝐾) Er (Base‘𝐺) ∧ 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ∧ 𝑥 ∈ 𝑟) → 𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
| 54 | 47, 51, 52, 53 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 56 | 16, 27, 55 | eqgid 19198 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (SubGrp‘𝐺) →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾) |
| 57 | 14, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾) |
| 58 | 57 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = 𝐾) |
| 59 | 46, 54, 58 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾)) |
| 60 | 4, 55 | qus0 19207 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (NrmSGrp‘𝐺) →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄)) |
| 61 | 12, 60 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄)) |
| 62 | 61 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → [(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄)) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) →
[(0g‘𝐺)](𝐺 ~QG 𝐾) = (0g‘𝑄)) |
| 64 | 59, 63 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ (𝐽‘𝑟) = 0 ) → 𝑟 = (0g‘𝑄)) |
| 65 | 62 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾) ↔ 𝑟 = (0g‘𝑄))) |
| 66 | 65 | biimpar 477 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → 𝑟 = [(0g‘𝐺)](𝐺 ~QG 𝐾)) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘𝑟) = (𝐽‘[(0g‘𝐺)](𝐺 ~QG 𝐾))) |
| 68 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
| 69 | 68 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
| 70 | 16, 55 | grpidcl 18983 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 71 | 8, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ (Base‘𝐺)) |
| 72 | 71 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (0g‘𝐺) ∈ (Base‘𝐺)) |
| 73 | 1, 69, 3, 4, 5, 72 | ghmquskerlem1 19301 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘[(0g‘𝐺)](𝐺 ~QG 𝐾)) = (𝐹‘(0g‘𝐺))) |
| 74 | 55, 1 | ghmid 19240 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐹‘(0g‘𝐺)) = 0 ) |
| 75 | 2, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘(0g‘𝐺)) = 0 ) |
| 76 | 75 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐹‘(0g‘𝐺)) = 0 ) |
| 77 | 67, 73, 76 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑟 = (0g‘𝑄)) → (𝐽‘𝑟) = 0 ) |
| 78 | 64, 77 | impbida 801 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ((𝐽‘𝑟) = 0 ↔ 𝑟 = (0g‘𝑄))) |
| 79 | 1, 68, 3, 4, 5, 48 | ghmquskerlem2 19303 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ∃𝑥 ∈ 𝑟 (𝐽‘𝑟) = (𝐹‘𝑥)) |
| 80 | 78, 79 | r19.29a 3162 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ((𝐽‘𝑟) = 0 ↔ 𝑟 = (0g‘𝑄))) |
| 81 | 80 | pm5.32da 579 |
. . . . . . . 8
⊢ (𝜑 → ((𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ) ↔ (𝑟 ∈ (Base‘𝑄) ∧ 𝑟 = (0g‘𝑄)))) |
| 82 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → 𝑟 = (0g‘𝑄)) |
| 83 | 4 | qusgrp 19204 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → 𝑄 ∈ Grp) |
| 84 | 12, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ Grp) |
| 85 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 86 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑄) = (0g‘𝑄) |
| 87 | 85, 86 | grpidcl 18983 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ Grp →
(0g‘𝑄)
∈ (Base‘𝑄)) |
| 88 | 84, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝑄) ∈ (Base‘𝑄)) |
| 89 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → (0g‘𝑄) ∈ (Base‘𝑄)) |
| 90 | 82, 89 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 = (0g‘𝑄)) → 𝑟 ∈ (Base‘𝑄)) |
| 91 | 90 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 = (0g‘𝑄) → 𝑟 ∈ (Base‘𝑄))) |
| 92 | 91 | pm4.71rd 562 |
. . . . . . . 8
⊢ (𝜑 → (𝑟 = (0g‘𝑄) ↔ (𝑟 ∈ (Base‘𝑄) ∧ 𝑟 = (0g‘𝑄)))) |
| 93 | 81, 92 | bitr4d 282 |
. . . . . . 7
⊢ (𝜑 → ((𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ) ↔ 𝑟 = (0g‘𝑄))) |
| 94 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
| 95 | 94 | imaexd 7938 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → (𝐹 “ 𝑞) ∈ V) |
| 96 | 95 | uniexd 7762 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘𝑄)) → ∪
(𝐹 “ 𝑞) ∈ V) |
| 97 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪
(𝐹 “ 𝑞))) |
| 98 | 21, 35 | fnfvelrnd 7102 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 99 | | ghmqusker.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) |
| 100 | 99 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ran 𝐹 = (Base‘𝐻)) |
| 101 | 98, 100 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ (Base‘𝐻)) |
| 102 | 37, 101 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘𝑟) ∈ (Base‘𝐻)) |
| 103 | 102, 79 | r19.29a 3162 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → (𝐽‘𝑟) ∈ (Base‘𝐻)) |
| 104 | 96, 97, 103 | fmpt2d 7144 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽:(Base‘𝑄)⟶(Base‘𝐻)) |
| 105 | 104 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 Fn (Base‘𝑄)) |
| 106 | | fniniseg 7080 |
. . . . . . . 8
⊢ (𝐽 Fn (Base‘𝑄) → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ (𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ))) |
| 107 | 105, 106 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ (𝑟 ∈ (Base‘𝑄) ∧ (𝐽‘𝑟) = 0 ))) |
| 108 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑟 ∈
{(0g‘𝑄)}
↔ 𝑟 =
(0g‘𝑄)) |
| 109 | 108 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑟 ∈ {(0g‘𝑄)} ↔ 𝑟 = (0g‘𝑄))) |
| 110 | 93, 107, 109 | 3bitr4d 311 |
. . . . . 6
⊢ (𝜑 → (𝑟 ∈ (◡𝐽 “ { 0 }) ↔ 𝑟 ∈
{(0g‘𝑄)})) |
| 111 | 110 | eqrdv 2735 |
. . . . 5
⊢ (𝜑 → (◡𝐽 “ { 0 }) =
{(0g‘𝑄)}) |
| 112 | 85, 17, 86, 1 | kerf1ghm 19265 |
. . . . . 6
⊢ (𝐽 ∈ (𝑄 GrpHom 𝐻) → (𝐽:(Base‘𝑄)–1-1→(Base‘𝐻) ↔ (◡𝐽 “ { 0 }) =
{(0g‘𝑄)})) |
| 113 | 112 | biimpar 477 |
. . . . 5
⊢ ((𝐽 ∈ (𝑄 GrpHom 𝐻) ∧ (◡𝐽 “ { 0 }) =
{(0g‘𝑄)})
→ 𝐽:(Base‘𝑄)–1-1→(Base‘𝐻)) |
| 114 | 6, 111, 113 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1→(Base‘𝐻)) |
| 115 | | f1f1orn 6859 |
. . . 4
⊢ (𝐽:(Base‘𝑄)–1-1→(Base‘𝐻) → 𝐽:(Base‘𝑄)–1-1-onto→ran
𝐽) |
| 116 | 114, 115 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1-onto→ran
𝐽) |
| 117 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) |
| 118 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝐾) ∈ V |
| 119 | 118 | ecelqsi 8813 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (Base‘𝐺) → [𝑥](𝐺 ~QG 𝐾) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
| 120 | 117, 119 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → [𝑥](𝐺 ~QG 𝐾) ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
| 121 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄)) |
| 122 | 120, 121 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → [𝑥](𝐺 ~QG 𝐾) ∈ (Base‘𝑄)) |
| 123 | | elqsi 8810 |
. . . . . . . . 9
⊢ (𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) → ∃𝑥 ∈ (Base‘𝐺)𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
| 124 | 50, 123 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → ∃𝑥 ∈ (Base‘𝐺)𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
| 125 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → 𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
| 126 | 125 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐽‘[𝑥](𝐺 ~QG 𝐾))) |
| 127 | 2 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
| 128 | 1, 127, 3, 4, 5, 117 | ghmquskerlem1 19301 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → (𝐽‘[𝑥](𝐺 ~QG 𝐾)) = (𝐹‘𝑥)) |
| 129 | 128 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘[𝑥](𝐺 ~QG 𝐾)) = (𝐹‘𝑥)) |
| 130 | 126, 129 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐹‘𝑥)) |
| 131 | 130 | 3impa 1110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → (𝐽‘𝑟) = (𝐹‘𝑥)) |
| 132 | 131 | eqeq1d 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑟 = [𝑥](𝐺 ~QG 𝐾)) → ((𝐽‘𝑟) = 𝑦 ↔ (𝐹‘𝑥) = 𝑦)) |
| 133 | 122, 124,
132 | rexxfrd2 5413 |
. . . . . . 7
⊢ (𝜑 → (∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦)) |
| 134 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝐽 Fn (Base‘𝑄) → (𝑦 ∈ ran 𝐽 ↔ ∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦)) |
| 135 | 105, 134 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ran 𝐽 ↔ ∃𝑟 ∈ (Base‘𝑄)(𝐽‘𝑟) = 𝑦)) |
| 136 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝐹 Fn (Base‘𝐺) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦)) |
| 137 | 20, 136 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝐺)(𝐹‘𝑥) = 𝑦)) |
| 138 | 133, 135,
137 | 3bitr4rd 312 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐽)) |
| 139 | 138 | eqrdv 2735 |
. . . . 5
⊢ (𝜑 → ran 𝐹 = ran 𝐽) |
| 140 | 139, 99 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ran 𝐽 = (Base‘𝐻)) |
| 141 | 140 | f1oeq3d 6845 |
. . 3
⊢ (𝜑 → (𝐽:(Base‘𝑄)–1-1-onto→ran
𝐽 ↔ 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻))) |
| 142 | 116, 141 | mpbid 232 |
. 2
⊢ (𝜑 → 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻)) |
| 143 | 85, 17 | isgim 19280 |
. 2
⊢ (𝐽 ∈ (𝑄 GrpIso 𝐻) ↔ (𝐽 ∈ (𝑄 GrpHom 𝐻) ∧ 𝐽:(Base‘𝑄)–1-1-onto→(Base‘𝐻))) |
| 144 | 6, 142, 143 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpIso 𝐻)) |