Step | Hyp | Ref
| Expression |
1 | | subgdisj.t |
. . . . . 6
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
2 | | subgdisj.a |
. . . . . 6
โข (๐ โ ๐ด โ ๐) |
3 | | subgdisj.c |
. . . . . 6
โข (๐ โ ๐ถ โ ๐) |
4 | | eqid 2732 |
. . . . . . 7
โข
(-gโ๐บ) = (-gโ๐บ) |
5 | 4 | subgsubcl 19011 |
. . . . . 6
โข ((๐ โ (SubGrpโ๐บ) โง ๐ด โ ๐ โง ๐ถ โ ๐) โ (๐ด(-gโ๐บ)๐ถ) โ ๐) |
6 | 1, 2, 3, 5 | syl3anc 1371 |
. . . . 5
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) โ ๐) |
7 | | subgdisj.j |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐ต) = (๐ถ + ๐ท)) |
8 | | subgdisj.s |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐โ๐)) |
9 | 8, 3 | sseldd 3982 |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ (๐โ๐)) |
10 | | subgdisj.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐) |
11 | | subgdisj.p |
. . . . . . . . . . 11
โข + =
(+gโ๐บ) |
12 | | subgdisj.z |
. . . . . . . . . . 11
โข ๐ = (Cntzโ๐บ) |
13 | 11, 12 | cntzi 19187 |
. . . . . . . . . 10
โข ((๐ถ โ (๐โ๐) โง ๐ต โ ๐) โ (๐ถ + ๐ต) = (๐ต + ๐ถ)) |
14 | 9, 10, 13 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (๐ถ + ๐ต) = (๐ต + ๐ถ)) |
15 | 7, 14 | oveq12d 7423 |
. . . . . . . 8
โข (๐ โ ((๐ด + ๐ต)(-gโ๐บ)(๐ถ + ๐ต)) = ((๐ถ + ๐ท)(-gโ๐บ)(๐ต + ๐ถ))) |
16 | | subgrcl 19005 |
. . . . . . . . . 10
โข (๐ โ (SubGrpโ๐บ) โ ๐บ โ Grp) |
17 | 1, 16 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐บ โ Grp) |
18 | | eqid 2732 |
. . . . . . . . . . . . 13
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
19 | 18 | subgss 19001 |
. . . . . . . . . . . 12
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (Baseโ๐บ)) |
21 | 20, 2 | sseldd 3982 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ (Baseโ๐บ)) |
22 | | subgdisj.u |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
23 | 18 | subgss 19001 |
. . . . . . . . . . . 12
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (Baseโ๐บ)) |
25 | 24, 10 | sseldd 3982 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ (Baseโ๐บ)) |
26 | 18, 11 | grpcl 18823 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ด โ (Baseโ๐บ) โง ๐ต โ (Baseโ๐บ)) โ (๐ด + ๐ต) โ (Baseโ๐บ)) |
27 | 17, 21, 25, 26 | syl3anc 1371 |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐ต) โ (Baseโ๐บ)) |
28 | 20, 3 | sseldd 3982 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ (Baseโ๐บ)) |
29 | 18, 11, 4 | grpsubsub4 18912 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ((๐ด + ๐ต) โ (Baseโ๐บ) โง ๐ต โ (Baseโ๐บ) โง ๐ถ โ (Baseโ๐บ))) โ (((๐ด + ๐ต)(-gโ๐บ)๐ต)(-gโ๐บ)๐ถ) = ((๐ด + ๐ต)(-gโ๐บ)(๐ถ + ๐ต))) |
30 | 17, 27, 25, 28, 29 | syl13anc 1372 |
. . . . . . . 8
โข (๐ โ (((๐ด + ๐ต)(-gโ๐บ)๐ต)(-gโ๐บ)๐ถ) = ((๐ด + ๐ต)(-gโ๐บ)(๐ถ + ๐ต))) |
31 | 7, 27 | eqeltrrd 2834 |
. . . . . . . . 9
โข (๐ โ (๐ถ + ๐ท) โ (Baseโ๐บ)) |
32 | 18, 11, 4 | grpsubsub4 18912 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ((๐ถ + ๐ท) โ (Baseโ๐บ) โง ๐ถ โ (Baseโ๐บ) โง ๐ต โ (Baseโ๐บ))) โ (((๐ถ + ๐ท)(-gโ๐บ)๐ถ)(-gโ๐บ)๐ต) = ((๐ถ + ๐ท)(-gโ๐บ)(๐ต + ๐ถ))) |
33 | 17, 31, 28, 25, 32 | syl13anc 1372 |
. . . . . . . 8
โข (๐ โ (((๐ถ + ๐ท)(-gโ๐บ)๐ถ)(-gโ๐บ)๐ต) = ((๐ถ + ๐ท)(-gโ๐บ)(๐ต + ๐ถ))) |
34 | 15, 30, 33 | 3eqtr4d 2782 |
. . . . . . 7
โข (๐ โ (((๐ด + ๐ต)(-gโ๐บ)๐ต)(-gโ๐บ)๐ถ) = (((๐ถ + ๐ท)(-gโ๐บ)๐ถ)(-gโ๐บ)๐ต)) |
35 | 18, 11, 4 | grppncan 18910 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ด โ (Baseโ๐บ) โง ๐ต โ (Baseโ๐บ)) โ ((๐ด + ๐ต)(-gโ๐บ)๐ต) = ๐ด) |
36 | 17, 21, 25, 35 | syl3anc 1371 |
. . . . . . . 8
โข (๐ โ ((๐ด + ๐ต)(-gโ๐บ)๐ต) = ๐ด) |
37 | 36 | oveq1d 7420 |
. . . . . . 7
โข (๐ โ (((๐ด + ๐ต)(-gโ๐บ)๐ต)(-gโ๐บ)๐ถ) = (๐ด(-gโ๐บ)๐ถ)) |
38 | | subgdisj.d |
. . . . . . . . . . 11
โข (๐ โ ๐ท โ ๐) |
39 | 11, 12 | cntzi 19187 |
. . . . . . . . . . 11
โข ((๐ถ โ (๐โ๐) โง ๐ท โ ๐) โ (๐ถ + ๐ท) = (๐ท + ๐ถ)) |
40 | 9, 38, 39 | syl2anc 584 |
. . . . . . . . . 10
โข (๐ โ (๐ถ + ๐ท) = (๐ท + ๐ถ)) |
41 | 40 | oveq1d 7420 |
. . . . . . . . 9
โข (๐ โ ((๐ถ + ๐ท)(-gโ๐บ)๐ถ) = ((๐ท + ๐ถ)(-gโ๐บ)๐ถ)) |
42 | 24, 38 | sseldd 3982 |
. . . . . . . . . 10
โข (๐ โ ๐ท โ (Baseโ๐บ)) |
43 | 18, 11, 4 | grppncan 18910 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ท โ (Baseโ๐บ) โง ๐ถ โ (Baseโ๐บ)) โ ((๐ท + ๐ถ)(-gโ๐บ)๐ถ) = ๐ท) |
44 | 17, 42, 28, 43 | syl3anc 1371 |
. . . . . . . . 9
โข (๐ โ ((๐ท + ๐ถ)(-gโ๐บ)๐ถ) = ๐ท) |
45 | 41, 44 | eqtrd 2772 |
. . . . . . . 8
โข (๐ โ ((๐ถ + ๐ท)(-gโ๐บ)๐ถ) = ๐ท) |
46 | 45 | oveq1d 7420 |
. . . . . . 7
โข (๐ โ (((๐ถ + ๐ท)(-gโ๐บ)๐ถ)(-gโ๐บ)๐ต) = (๐ท(-gโ๐บ)๐ต)) |
47 | 34, 37, 46 | 3eqtr3d 2780 |
. . . . . 6
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) = (๐ท(-gโ๐บ)๐ต)) |
48 | 4 | subgsubcl 19011 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ๐ท โ ๐ โง ๐ต โ ๐) โ (๐ท(-gโ๐บ)๐ต) โ ๐) |
49 | 22, 38, 10, 48 | syl3anc 1371 |
. . . . . 6
โข (๐ โ (๐ท(-gโ๐บ)๐ต) โ ๐) |
50 | 47, 49 | eqeltrd 2833 |
. . . . 5
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) โ ๐) |
51 | 6, 50 | elind 4193 |
. . . 4
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) โ (๐ โฉ ๐)) |
52 | | subgdisj.i |
. . . 4
โข (๐ โ (๐ โฉ ๐) = { 0 }) |
53 | 51, 52 | eleqtrd 2835 |
. . 3
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) โ { 0 }) |
54 | | elsni 4644 |
. . 3
โข ((๐ด(-gโ๐บ)๐ถ) โ { 0 } โ (๐ด(-gโ๐บ)๐ถ) = 0 ) |
55 | 53, 54 | syl 17 |
. 2
โข (๐ โ (๐ด(-gโ๐บ)๐ถ) = 0 ) |
56 | | subgdisj.o |
. . . 4
โข 0 =
(0gโ๐บ) |
57 | 18, 56, 4 | grpsubeq0 18905 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ (Baseโ๐บ) โง ๐ถ โ (Baseโ๐บ)) โ ((๐ด(-gโ๐บ)๐ถ) = 0 โ ๐ด = ๐ถ)) |
58 | 17, 21, 28, 57 | syl3anc 1371 |
. 2
โข (๐ โ ((๐ด(-gโ๐บ)๐ถ) = 0 โ ๐ด = ๐ถ)) |
59 | 55, 58 | mpbid 231 |
1
โข (๐ โ ๐ด = ๐ถ) |