Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
โข ((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โ ๐ โ (SubGrpโ๐)) |
2 | | simplr 767 |
. . . . . . . . 9
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ โ ๐) |
3 | | simprr 771 |
. . . . . . . . 9
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ฆ โ ๐) |
4 | 2, 3 | sseldd 3982 |
. . . . . . . 8
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ฆ โ ๐) |
5 | | eqid 2732 |
. . . . . . . . . 10
โข
(Baseโ๐) =
(Baseโ๐) |
6 | | eqid 2732 |
. . . . . . . . . 10
โข
(Cntzโ๐) =
(Cntzโ๐) |
7 | 5, 6 | cntrval 19177 |
. . . . . . . . 9
โข
((Cntzโ๐)โ(Baseโ๐)) = (Cntrโ๐) |
8 | | cntrnsg.z |
. . . . . . . . 9
โข ๐ = (Cntrโ๐) |
9 | 7, 8 | eqtr4i 2763 |
. . . . . . . 8
โข
((Cntzโ๐)โ(Baseโ๐)) = ๐ |
10 | 4, 9 | eleqtrrdi 2844 |
. . . . . . 7
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ฆ โ ((Cntzโ๐)โ(Baseโ๐))) |
11 | | simprl 769 |
. . . . . . 7
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ฅ โ (Baseโ๐)) |
12 | | eqid 2732 |
. . . . . . . 8
โข
(+gโ๐) = (+gโ๐) |
13 | 12, 6 | cntzi 19187 |
. . . . . . 7
โข ((๐ฆ โ ((Cntzโ๐)โ(Baseโ๐)) โง ๐ฅ โ (Baseโ๐)) โ (๐ฆ(+gโ๐)๐ฅ) = (๐ฅ(+gโ๐)๐ฆ)) |
14 | 10, 11, 13 | syl2anc 584 |
. . . . . 6
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ (๐ฆ(+gโ๐)๐ฅ) = (๐ฅ(+gโ๐)๐ฆ)) |
15 | 14 | oveq1d 7420 |
. . . . 5
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ((๐ฆ(+gโ๐)๐ฅ)(-gโ๐)๐ฅ) = ((๐ฅ(+gโ๐)๐ฆ)(-gโ๐)๐ฅ)) |
16 | | subgrcl 19005 |
. . . . . . 7
โข (๐ โ (SubGrpโ๐) โ ๐ โ Grp) |
17 | 16 | ad2antrr 724 |
. . . . . 6
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ โ Grp) |
18 | 5 | subgss 19001 |
. . . . . . . 8
โข (๐ โ (SubGrpโ๐) โ ๐ โ (Baseโ๐)) |
19 | 18 | ad2antrr 724 |
. . . . . . 7
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ โ (Baseโ๐)) |
20 | 19, 3 | sseldd 3982 |
. . . . . 6
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ๐ฆ โ (Baseโ๐)) |
21 | | eqid 2732 |
. . . . . . 7
โข
(-gโ๐) = (-gโ๐) |
22 | 5, 12, 21 | grppncan 18910 |
. . . . . 6
โข ((๐ โ Grp โง ๐ฆ โ (Baseโ๐) โง ๐ฅ โ (Baseโ๐)) โ ((๐ฆ(+gโ๐)๐ฅ)(-gโ๐)๐ฅ) = ๐ฆ) |
23 | 17, 20, 11, 22 | syl3anc 1371 |
. . . . 5
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ((๐ฆ(+gโ๐)๐ฅ)(-gโ๐)๐ฅ) = ๐ฆ) |
24 | 15, 23 | eqtr3d 2774 |
. . . 4
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ((๐ฅ(+gโ๐)๐ฆ)(-gโ๐)๐ฅ) = ๐ฆ) |
25 | 24, 3 | eqeltrd 2833 |
. . 3
โข (((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โง (๐ฅ โ (Baseโ๐) โง ๐ฆ โ ๐)) โ ((๐ฅ(+gโ๐)๐ฆ)(-gโ๐)๐ฅ) โ ๐) |
26 | 25 | ralrimivva 3200 |
. 2
โข ((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โ โ๐ฅ โ (Baseโ๐)โ๐ฆ โ ๐ ((๐ฅ(+gโ๐)๐ฆ)(-gโ๐)๐ฅ) โ ๐) |
27 | 5, 12, 21 | isnsg3 19034 |
. 2
โข (๐ โ (NrmSGrpโ๐) โ (๐ โ (SubGrpโ๐) โง โ๐ฅ โ (Baseโ๐)โ๐ฆ โ ๐ ((๐ฅ(+gโ๐)๐ฆ)(-gโ๐)๐ฅ) โ ๐)) |
28 | 1, 26, 27 | sylanbrc 583 |
1
โข ((๐ โ (SubGrpโ๐) โง ๐ โ ๐) โ ๐ โ (NrmSGrpโ๐)) |