Step | Hyp | Ref
| Expression |
1 | | simp3 1139 |
. . . . . . . . 9
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ ๐ โ (๐โ๐)) |
2 | 1 | sselda 3983 |
. . . . . . . 8
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โง ๐ โ ๐) โ ๐ โ (๐โ๐)) |
3 | 2 | adantrr 716 |
. . . . . . 7
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ (๐โ๐)) |
4 | | simprr 772 |
. . . . . . 7
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
5 | | eqid 2733 |
. . . . . . . 8
โข
(+gโ๐บ) = (+gโ๐บ) |
6 | | lsmsubg.z |
. . . . . . . 8
โข ๐ = (Cntzโ๐บ) |
7 | 5, 6 | cntzi 19193 |
. . . . . . 7
โข ((๐ โ (๐โ๐) โง ๐ โ ๐) โ (๐(+gโ๐บ)๐) = (๐(+gโ๐บ)๐)) |
8 | 3, 4, 7 | syl2anc 585 |
. . . . . 6
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(+gโ๐บ)๐) = (๐(+gโ๐บ)๐)) |
9 | 8 | eqeq2d 2744 |
. . . . 5
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ฅ = (๐(+gโ๐บ)๐) โ ๐ฅ = (๐(+gโ๐บ)๐))) |
10 | 9 | 2rexbidva 3218 |
. . . 4
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
11 | | rexcom 3288 |
. . . 4
โข
(โ๐ โ
๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐)) |
12 | 10, 11 | bitrdi 287 |
. . 3
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
13 | | lsmsubg.p |
. . . . 5
โข โ =
(LSSumโ๐บ) |
14 | 5, 13 | lsmelval 19517 |
. . . 4
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
15 | 14 | 3adant3 1133 |
. . 3
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (๐ฅ โ (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
16 | 5, 13 | lsmelval 19517 |
. . . . 5
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
17 | 16 | ancoms 460 |
. . . 4
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
18 | 17 | 3adant3 1133 |
. . 3
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (๐ฅ โ (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ฅ = (๐(+gโ๐บ)๐))) |
19 | 12, 15, 18 | 3bitr4d 311 |
. 2
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (๐ฅ โ (๐ โ ๐) โ ๐ฅ โ (๐ โ ๐))) |
20 | 19 | eqrdv 2731 |
1
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (๐ โ ๐) = (๐ โ ๐)) |