Proof of Theorem subgdisj1
| Step | Hyp | Ref
| Expression |
| 1 | | subgdisj.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
| 2 | | subgdisj.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
| 3 | | subgdisj.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 5 | 4 | subgsubcl 19155 |
. . . . . 6
⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑇 ∧ 𝐶 ∈ 𝑇) → (𝐴(-g‘𝐺)𝐶) ∈ 𝑇) |
| 6 | 1, 2, 3, 5 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ 𝑇) |
| 7 | | subgdisj.j |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) |
| 8 | | subgdisj.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
| 9 | 8, 3 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (𝑍‘𝑈)) |
| 10 | | subgdisj.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| 11 | | subgdisj.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
| 12 | | subgdisj.z |
. . . . . . . . . . 11
⊢ 𝑍 = (Cntz‘𝐺) |
| 13 | 11, 12 | cntzi 19347 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑍‘𝑈) ∧ 𝐵 ∈ 𝑈) → (𝐶 + 𝐵) = (𝐵 + 𝐶)) |
| 14 | 9, 10, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + 𝐵) = (𝐵 + 𝐶)) |
| 15 | 7, 14 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵)) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
| 16 | | subgrcl 19149 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 17 | 1, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 18 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 19 | 18 | subgss 19145 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝑇 ⊆ (Base‘𝐺)) |
| 20 | 1, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺)) |
| 21 | 20, 2 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Base‘𝐺)) |
| 22 | | subgdisj.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
| 23 | 18 | subgss 19145 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐺)) |
| 25 | 24, 10 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (Base‘𝐺)) |
| 26 | 18, 11 | grpcl 18959 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺)) → (𝐴 + 𝐵) ∈ (Base‘𝐺)) |
| 27 | 17, 21, 25, 26 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝐵) ∈ (Base‘𝐺)) |
| 28 | 20, 3 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐺)) |
| 29 | 18, 11, 4 | grpsubsub4 19051 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ((𝐴 + 𝐵) ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺))) → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵))) |
| 30 | 17, 27, 25, 28, 29 | syl13anc 1374 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵))) |
| 31 | 7, 27 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + 𝐷) ∈ (Base‘𝐺)) |
| 32 | 18, 11, 4 | grpsubsub4 19051 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ((𝐶 + 𝐷) ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺))) → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
| 33 | 17, 31, 28, 25, 32 | syl13anc 1374 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
| 34 | 15, 30, 33 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵)) |
| 35 | 18, 11, 4 | grppncan 19049 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺)) → ((𝐴 + 𝐵)(-g‘𝐺)𝐵) = 𝐴) |
| 36 | 17, 21, 25, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝐺)𝐵) = 𝐴) |
| 37 | 36 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = (𝐴(-g‘𝐺)𝐶)) |
| 38 | | subgdisj.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
| 39 | 11, 12 | cntzi 19347 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑍‘𝑈) ∧ 𝐷 ∈ 𝑈) → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
| 40 | 9, 38, 39 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 + 𝐷)(-g‘𝐺)𝐶) = ((𝐷 + 𝐶)(-g‘𝐺)𝐶)) |
| 42 | 24, 38 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Base‘𝐺)) |
| 43 | 18, 11, 4 | grppncan 19049 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐷 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺)) → ((𝐷 + 𝐶)(-g‘𝐺)𝐶) = 𝐷) |
| 44 | 17, 42, 28, 43 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 + 𝐶)(-g‘𝐺)𝐶) = 𝐷) |
| 45 | 41, 44 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 + 𝐷)(-g‘𝐺)𝐶) = 𝐷) |
| 46 | 45 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = (𝐷(-g‘𝐺)𝐵)) |
| 47 | 34, 37, 46 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) = (𝐷(-g‘𝐺)𝐵)) |
| 48 | 4 | subgsubcl 19155 |
. . . . . . 7
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ 𝐷 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐷(-g‘𝐺)𝐵) ∈ 𝑈) |
| 49 | 22, 38, 10, 48 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐷(-g‘𝐺)𝐵) ∈ 𝑈) |
| 50 | 47, 49 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ 𝑈) |
| 51 | 6, 50 | elind 4200 |
. . . 4
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ (𝑇 ∩ 𝑈)) |
| 52 | | subgdisj.i |
. . . 4
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
| 53 | 51, 52 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ { 0 }) |
| 54 | | elsni 4643 |
. . 3
⊢ ((𝐴(-g‘𝐺)𝐶) ∈ { 0 } → (𝐴(-g‘𝐺)𝐶) = 0 ) |
| 55 | 53, 54 | syl 17 |
. 2
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) = 0 ) |
| 56 | | subgdisj.o |
. . . 4
⊢ 0 =
(0g‘𝐺) |
| 57 | 18, 56, 4 | grpsubeq0 19044 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺)) → ((𝐴(-g‘𝐺)𝐶) = 0 ↔ 𝐴 = 𝐶)) |
| 58 | 17, 21, 28, 57 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝐴(-g‘𝐺)𝐶) = 0 ↔ 𝐴 = 𝐶)) |
| 59 | 55, 58 | mpbid 232 |
1
⊢ (𝜑 → 𝐴 = 𝐶) |