Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
โข (๐ = ๐
โ (mulGrpโ๐) = (mulGrpโ๐
)) |
2 | | isring.g |
. . . . . 6
โข ๐บ = (mulGrpโ๐
) |
3 | 1, 2 | eqtr4di 2795 |
. . . . 5
โข (๐ = ๐
โ (mulGrpโ๐) = ๐บ) |
4 | 3 | eleq1d 2823 |
. . . 4
โข (๐ = ๐
โ ((mulGrpโ๐) โ Mnd โ ๐บ โ Mnd)) |
5 | | fvexd 6862 |
. . . . 5
โข (๐ = ๐
โ (Baseโ๐) โ V) |
6 | | fveq2 6847 |
. . . . . 6
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
7 | | isring.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
8 | 6, 7 | eqtr4di 2795 |
. . . . 5
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
9 | | fvexd 6862 |
. . . . . 6
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) โ V) |
10 | | simpl 484 |
. . . . . . . 8
โข ((๐ = ๐
โง ๐ = ๐ต) โ ๐ = ๐
) |
11 | 10 | fveq2d 6851 |
. . . . . . 7
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) = (+gโ๐
)) |
12 | | isring.p |
. . . . . . 7
โข + =
(+gโ๐
) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . 6
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) = + ) |
14 | | fvexd 6862 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐)
โ V) |
15 | | simpll 766 |
. . . . . . . . 9
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ ๐ = ๐
) |
16 | 15 | fveq2d 6851 |
. . . . . . . 8
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐) =
(.rโ๐
)) |
17 | | isring.t |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐) =
ยท
) |
19 | | simpllr 775 |
. . . . . . . 8
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ = ๐ต) |
20 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ก = ยท ) |
21 | | eqidd 2738 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ฅ = ๐ฅ) |
22 | | simplr 768 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ = + ) |
23 | 22 | oveqd 7379 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฆ๐๐ง) = (๐ฆ + ๐ง)) |
24 | 20, 21, 23 | oveq123d 7383 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก(๐ฆ๐๐ง)) = (๐ฅ ยท (๐ฆ + ๐ง))) |
25 | 20 | oveqd 7379 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก๐ฆ) = (๐ฅ ยท ๐ฆ)) |
26 | 20 | oveqd 7379 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก๐ง) = (๐ฅ ยท ๐ง)) |
27 | 22, 25, 26 | oveq123d 7383 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
28 | 24, 27 | eqeq12d 2753 |
. . . . . . . . . . 11
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
29 | 22 | oveqd 7379 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐๐ฆ) = (๐ฅ + ๐ฆ)) |
30 | | eqidd 2738 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ง = ๐ง) |
31 | 20, 29, 30 | oveq123d 7383 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ + ๐ฆ) ยท ๐ง)) |
32 | 20 | oveqd 7379 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฆ๐ก๐ง) = (๐ฆ ยท ๐ง)) |
33 | 22, 26, 32 | oveq123d 7383 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
34 | 31, 33 | eqeq12d 2753 |
. . . . . . . . . . 11
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
35 | 28, 34 | anbi12d 632 |
. . . . . . . . . 10
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
36 | 19, 35 | raleqbidv 3322 |
. . . . . . . . 9
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
37 | 19, 36 | raleqbidv 3322 |
. . . . . . . 8
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
38 | 19, 37 | raleqbidv 3322 |
. . . . . . 7
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
39 | 14, 18, 38 | sbcied2 3791 |
. . . . . 6
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
([(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
40 | 9, 13, 39 | sbcied2 3791 |
. . . . 5
โข ((๐ = ๐
โง ๐ = ๐ต) โ ([(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
41 | 5, 8, 40 | sbcied2 3791 |
. . . 4
โข (๐ = ๐
โ ([(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
42 | 4, 41 | anbi12d 632 |
. . 3
โข (๐ = ๐
โ (((mulGrpโ๐) โ Mnd โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)))) โ (๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
43 | | df-ring 19973 |
. . 3
โข Ring =
{๐ โ Grp โฃ
((mulGrpโ๐) โ
Mnd โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))))} |
44 | 42, 43 | elrab2 3653 |
. 2
โข (๐
โ Ring โ (๐
โ Grp โง (๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
45 | | 3anass 1096 |
. 2
โข ((๐
โ Grp โง ๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) โ (๐
โ Grp โง (๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
46 | 44, 45 | bitr4i 278 |
1
โข (๐
โ Ring โ (๐
โ Grp โง ๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |