Step | Hyp | Ref
| Expression |
1 | | srgdilem.b |
. . . . . . . . . . 11
โข ๐ต = (Baseโ๐
) |
2 | | eqid 2733 |
. . . . . . . . . . 11
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
3 | | srgdilem.p |
. . . . . . . . . . 11
โข + =
(+gโ๐
) |
4 | | srgdilem.t |
. . . . . . . . . . 11
โข ยท =
(.rโ๐
) |
5 | | eqid 2733 |
. . . . . . . . . . 11
โข
(0gโ๐
) = (0gโ๐
) |
6 | 1, 2, 3, 4, 5 | issrg 20011 |
. . . . . . . . . 10
โข (๐
โ SRing โ (๐
โ CMnd โง
(mulGrpโ๐
) โ Mnd
โง โ๐ฅ โ
๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (((0gโ๐
) ยท ๐ฅ) = (0gโ๐
) โง (๐ฅ ยท
(0gโ๐
)) =
(0gโ๐
))))) |
7 | 6 | simp3bi 1148 |
. . . . . . . . 9
โข (๐
โ SRing โ
โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (((0gโ๐
) ยท ๐ฅ) = (0gโ๐
) โง (๐ฅ ยท
(0gโ๐
)) =
(0gโ๐
)))) |
8 | 7 | r19.21bi 3249 |
. . . . . . . 8
โข ((๐
โ SRing โง ๐ฅ โ ๐ต) โ (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (((0gโ๐
) ยท ๐ฅ) = (0gโ๐
) โง (๐ฅ ยท
(0gโ๐
)) =
(0gโ๐
)))) |
9 | 8 | simpld 496 |
. . . . . . 7
โข ((๐
โ SRing โง ๐ฅ โ ๐ต) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
10 | 9 | 3ad2antr1 1189 |
. . . . . 6
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
11 | | simpr2 1196 |
. . . . . 6
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ๐ฆ โ ๐ต) |
12 | | rsp 3245 |
. . . . . 6
โข
(โ๐ฆ โ
๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โ (๐ฆ โ ๐ต โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
13 | 10, 11, 12 | sylc 65 |
. . . . 5
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
14 | | simpr3 1197 |
. . . . 5
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ๐ง โ ๐ต) |
15 | | rsp 3245 |
. . . . 5
โข
(โ๐ง โ
๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โ (๐ง โ ๐ต โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
16 | 13, 14, 15 | sylc 65 |
. . . 4
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
17 | 16 | simpld 496 |
. . 3
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
18 | 17 | caovdig 7621 |
. 2
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
19 | 16 | simprd 497 |
. . 3
โข ((๐
โ SRing โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
20 | 19 | caovdirg 7624 |
. 2
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
21 | 18, 20 | jca 513 |
1
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |