Step | Hyp | Ref
| Expression |
1 | | ringdilem.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐
) |
2 | | eqid 2733 |
. . . . . . . . . 10
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
3 | | ringdilem.p |
. . . . . . . . . 10
โข + =
(+gโ๐
) |
4 | | ringdilem.t |
. . . . . . . . . 10
โข ยท =
(.rโ๐
) |
5 | 1, 2, 3, 4 | isring 19976 |
. . . . . . . . 9
โข (๐
โ Ring โ (๐
โ Grp โง
(mulGrpโ๐
) โ Mnd
โง โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
6 | 5 | simp3bi 1148 |
. . . . . . . 8
โข (๐
โ Ring โ
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
7 | 6 | adantr 482 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
8 | | simpr1 1195 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ๐ฅ โ ๐ต) |
9 | | rsp 3229 |
. . . . . . 7
โข
(โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โ (๐ฅ โ ๐ต โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
10 | 7, 8, 9 | sylc 65 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
11 | | simpr2 1196 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ๐ฆ โ ๐ต) |
12 | | rsp 3229 |
. . . . . 6
โข
(โ๐ฆ โ
๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โ (๐ฆ โ ๐ต โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
13 | 10, 11, 12 | sylc 65 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
14 | | simpr3 1197 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ๐ง โ ๐ต) |
15 | | rsp 3229 |
. . . . 5
โข
(โ๐ง โ
๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โ (๐ง โ ๐ต โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
16 | 13, 14, 15 | sylc 65 |
. . . 4
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
17 | 16 | simpld 496 |
. . 3
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
18 | 17 | caovdig 7572 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
19 | 16 | simprd 497 |
. . 3
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
20 | 19 | caovdirg 7575 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
21 | 18, 20 | jca 513 |
1
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |