Proof of Theorem subgdisj1
Step | Hyp | Ref
| Expression |
1 | | subgdisj.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
2 | | subgdisj.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
3 | | subgdisj.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
4 | | eqid 2738 |
. . . . . . 7
⊢
(-g‘𝐺) = (-g‘𝐺) |
5 | 4 | subgsubcl 18766 |
. . . . . 6
⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑇 ∧ 𝐶 ∈ 𝑇) → (𝐴(-g‘𝐺)𝐶) ∈ 𝑇) |
6 | 1, 2, 3, 5 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ 𝑇) |
7 | | subgdisj.j |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) |
8 | | subgdisj.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
9 | 8, 3 | sseldd 3922 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (𝑍‘𝑈)) |
10 | | subgdisj.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
11 | | subgdisj.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
12 | | subgdisj.z |
. . . . . . . . . . 11
⊢ 𝑍 = (Cntz‘𝐺) |
13 | 11, 12 | cntzi 18935 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑍‘𝑈) ∧ 𝐵 ∈ 𝑈) → (𝐶 + 𝐵) = (𝐵 + 𝐶)) |
14 | 9, 10, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + 𝐵) = (𝐵 + 𝐶)) |
15 | 7, 14 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵)) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
16 | | subgrcl 18760 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
17 | 1, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
18 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
19 | 18 | subgss 18756 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝑇 ⊆ (Base‘𝐺)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺)) |
21 | 20, 2 | sseldd 3922 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (Base‘𝐺)) |
22 | | subgdisj.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
23 | 18 | subgss 18756 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐺)) |
25 | 24, 10 | sseldd 3922 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (Base‘𝐺)) |
26 | 18, 11 | grpcl 18585 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺)) → (𝐴 + 𝐵) ∈ (Base‘𝐺)) |
27 | 17, 21, 25, 26 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝐵) ∈ (Base‘𝐺)) |
28 | 20, 3 | sseldd 3922 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐺)) |
29 | 18, 11, 4 | grpsubsub4 18668 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ((𝐴 + 𝐵) ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺))) → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵))) |
30 | 17, 27, 25, 28, 29 | syl13anc 1371 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = ((𝐴 + 𝐵)(-g‘𝐺)(𝐶 + 𝐵))) |
31 | 7, 27 | eqeltrrd 2840 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + 𝐷) ∈ (Base‘𝐺)) |
32 | 18, 11, 4 | grpsubsub4 18668 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ((𝐶 + 𝐷) ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺))) → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
33 | 17, 31, 28, 25, 32 | syl13anc 1371 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = ((𝐶 + 𝐷)(-g‘𝐺)(𝐵 + 𝐶))) |
34 | 15, 30, 33 | 3eqtr4d 2788 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵)) |
35 | 18, 11, 4 | grppncan 18666 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺)) → ((𝐴 + 𝐵)(-g‘𝐺)𝐵) = 𝐴) |
36 | 17, 21, 25, 35 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝐺)𝐵) = 𝐴) |
37 | 36 | oveq1d 7290 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 + 𝐵)(-g‘𝐺)𝐵)(-g‘𝐺)𝐶) = (𝐴(-g‘𝐺)𝐶)) |
38 | | subgdisj.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
39 | 11, 12 | cntzi 18935 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑍‘𝑈) ∧ 𝐷 ∈ 𝑈) → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
40 | 9, 38, 39 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
41 | 40 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 + 𝐷)(-g‘𝐺)𝐶) = ((𝐷 + 𝐶)(-g‘𝐺)𝐶)) |
42 | 24, 38 | sseldd 3922 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Base‘𝐺)) |
43 | 18, 11, 4 | grppncan 18666 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐷 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺)) → ((𝐷 + 𝐶)(-g‘𝐺)𝐶) = 𝐷) |
44 | 17, 42, 28, 43 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 + 𝐶)(-g‘𝐺)𝐶) = 𝐷) |
45 | 41, 44 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 + 𝐷)(-g‘𝐺)𝐶) = 𝐷) |
46 | 45 | oveq1d 7290 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 + 𝐷)(-g‘𝐺)𝐶)(-g‘𝐺)𝐵) = (𝐷(-g‘𝐺)𝐵)) |
47 | 34, 37, 46 | 3eqtr3d 2786 |
. . . . . 6
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) = (𝐷(-g‘𝐺)𝐵)) |
48 | 4 | subgsubcl 18766 |
. . . . . . 7
⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ 𝐷 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐷(-g‘𝐺)𝐵) ∈ 𝑈) |
49 | 22, 38, 10, 48 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝐷(-g‘𝐺)𝐵) ∈ 𝑈) |
50 | 47, 49 | eqeltrd 2839 |
. . . . 5
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ 𝑈) |
51 | 6, 50 | elind 4128 |
. . . 4
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ (𝑇 ∩ 𝑈)) |
52 | | subgdisj.i |
. . . 4
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
53 | 51, 52 | eleqtrd 2841 |
. . 3
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) ∈ { 0 }) |
54 | | elsni 4578 |
. . 3
⊢ ((𝐴(-g‘𝐺)𝐶) ∈ { 0 } → (𝐴(-g‘𝐺)𝐶) = 0 ) |
55 | 53, 54 | syl 17 |
. 2
⊢ (𝜑 → (𝐴(-g‘𝐺)𝐶) = 0 ) |
56 | | subgdisj.o |
. . . 4
⊢ 0 =
(0g‘𝐺) |
57 | 18, 56, 4 | grpsubeq0 18661 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝐶 ∈ (Base‘𝐺)) → ((𝐴(-g‘𝐺)𝐶) = 0 ↔ 𝐴 = 𝐶)) |
58 | 17, 21, 28, 57 | syl3anc 1370 |
. 2
⊢ (𝜑 → ((𝐴(-g‘𝐺)𝐶) = 0 ↔ 𝐴 = 𝐶)) |
59 | 55, 58 | mpbid 231 |
1
⊢ (𝜑 → 𝐴 = 𝐶) |