Step | Hyp | Ref
| Expression |
1 | | issrg.g |
. . . . . 6
โข ๐บ = (mulGrpโ๐
) |
2 | 1 | eleq1i 2825 |
. . . . 5
โข (๐บ โ Mnd โ
(mulGrpโ๐
) โ
Mnd) |
3 | 2 | bicomi 223 |
. . . 4
โข
((mulGrpโ๐
)
โ Mnd โ ๐บ โ
Mnd) |
4 | | issrg.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
5 | 4 | fvexi 6860 |
. . . . 5
โข ๐ต โ V |
6 | | issrg.p |
. . . . . 6
โข + =
(+gโ๐
) |
7 | 6 | fvexi 6860 |
. . . . 5
โข + โ
V |
8 | | issrg.t |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
9 | 8 | fvexi 6860 |
. . . . . . 7
โข ยท โ
V |
10 | 9 | a1i 11 |
. . . . . 6
โข ((๐ = ๐ต โง ๐ = + ) โ ยท โ
V) |
11 | | issrg.0 |
. . . . . . . . 9
โข 0 =
(0gโ๐
) |
12 | 11 | fvexi 6860 |
. . . . . . . 8
โข 0 โ
V |
13 | 12 | a1i 11 |
. . . . . . 7
โข (((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โ 0 โ
V) |
14 | | simplll 774 |
. . . . . . . 8
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ = ๐ต) |
15 | | simplr 768 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ก = ยท ) |
16 | | eqidd 2734 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ฅ = ๐ฅ) |
17 | | simpllr 775 |
. . . . . . . . . . . . . . 15
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ = + ) |
18 | 17 | oveqd 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฆ๐๐ง) = (๐ฆ + ๐ง)) |
19 | 15, 16, 18 | oveq123d 7382 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฅ๐ก(๐ฆ๐๐ง)) = (๐ฅ ยท (๐ฆ + ๐ง))) |
20 | 15 | oveqd 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฅ๐ก๐ฆ) = (๐ฅ ยท ๐ฆ)) |
21 | 15 | oveqd 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฅ๐ก๐ง) = (๐ฅ ยท ๐ง)) |
22 | 17, 20, 21 | oveq123d 7382 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
23 | 19, 22 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
24 | 17 | oveqd 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฅ๐๐ฆ) = (๐ฅ + ๐ฆ)) |
25 | | eqidd 2734 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ง = ๐ง) |
26 | 15, 24, 25 | oveq123d 7382 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ + ๐ฆ) ยท ๐ง)) |
27 | 15 | oveqd 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฆ๐ก๐ง) = (๐ฆ ยท ๐ง)) |
28 | 17, 21, 27 | oveq123d 7382 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
29 | 26, 28 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
30 | 23, 29 | anbi12d 632 |
. . . . . . . . . . 11
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
31 | 14, 30 | raleqbidv 3318 |
. . . . . . . . . 10
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
32 | 14, 31 | raleqbidv 3318 |
. . . . . . . . 9
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
33 | | simpr 486 |
. . . . . . . . . . . 12
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ๐ = 0 ) |
34 | 15, 33, 16 | oveq123d 7382 |
. . . . . . . . . . 11
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐๐ก๐ฅ) = ( 0 ยท ๐ฅ)) |
35 | 34, 33 | eqeq12d 2749 |
. . . . . . . . . 10
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐๐ก๐ฅ) = ๐ โ ( 0 ยท ๐ฅ) = 0 )) |
36 | 15, 16, 33 | oveq123d 7382 |
. . . . . . . . . . 11
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (๐ฅ๐ก๐) = (๐ฅ ยท 0 )) |
37 | 36, 33 | eqeq12d 2749 |
. . . . . . . . . 10
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((๐ฅ๐ก๐) = ๐ โ (๐ฅ ยท 0 ) = 0 )) |
38 | 35, 37 | anbi12d 632 |
. . . . . . . . 9
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐) โ (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 ))) |
39 | 32, 38 | anbi12d 632 |
. . . . . . . 8
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ ((โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |
40 | 14, 39 | raleqbidv 3318 |
. . . . . . 7
โข ((((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โง ๐ = 0 ) โ (โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |
41 | 13, 40 | sbcied 3788 |
. . . . . 6
โข (((๐ = ๐ต โง ๐ = + ) โง ๐ก = ยท ) โ ([
0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |
42 | 10, 41 | sbcied 3788 |
. . . . 5
โข ((๐ = ๐ต โง ๐ = + ) โ ([ ยท /
๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |
43 | 5, 7, 42 | sbc2ie 3826 |
. . . 4
โข
([๐ต / ๐][ + / ๐][ ยท /
๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 ))) |
44 | 3, 43 | anbi12i 628 |
. . 3
โข
(((mulGrpโ๐
)
โ Mnd โง [๐ต
/ ๐][ + / ๐][ ยท /
๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐))) โ (๐บ โ Mnd โง โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |
45 | 44 | anbi2i 624 |
. 2
โข ((๐
โ CMnd โง
((mulGrpโ๐
) โ
Mnd โง [๐ต / ๐][ + / ๐][ ยท /
๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))) โ (๐
โ CMnd โง (๐บ โ Mnd โง โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 ))))) |
46 | | fveq2 6846 |
. . . . 5
โข (๐ = ๐
โ (mulGrpโ๐) = (mulGrpโ๐
)) |
47 | 46 | eleq1d 2819 |
. . . 4
โข (๐ = ๐
โ ((mulGrpโ๐) โ Mnd โ (mulGrpโ๐
) โ Mnd)) |
48 | | fveq2 6846 |
. . . . . 6
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
49 | 48, 4 | eqtr4di 2791 |
. . . . 5
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
50 | | fveq2 6846 |
. . . . . . 7
โข (๐ = ๐
โ (+gโ๐) = (+gโ๐
)) |
51 | 50, 6 | eqtr4di 2791 |
. . . . . 6
โข (๐ = ๐
โ (+gโ๐) = + ) |
52 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
53 | 52, 8 | eqtr4di 2791 |
. . . . . . 7
โข (๐ = ๐
โ (.rโ๐) = ยท ) |
54 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = ๐
โ (0gโ๐) = (0gโ๐
)) |
55 | 54, 11 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ = ๐
โ (0gโ๐) = 0 ) |
56 | 55 | sbceq1d 3748 |
. . . . . . 7
โข (๐ = ๐
โ ([(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ [ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))) |
57 | 53, 56 | sbceqbid 3750 |
. . . . . 6
โข (๐ = ๐
โ ([(.rโ๐) / ๐ก][(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ [ ยท / ๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))) |
58 | 51, 57 | sbceqbid 3750 |
. . . . 5
โข (๐ = ๐
โ ([(+gโ๐) / ๐][(.rโ๐) / ๐ก][(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ [ + / ๐][ ยท / ๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))) |
59 | 49, 58 | sbceqbid 3750 |
. . . 4
โข (๐ = ๐
โ ([(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก][(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)) โ [๐ต / ๐][ + / ๐][ ยท / ๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))) |
60 | 47, 59 | anbi12d 632 |
. . 3
โข (๐ = ๐
โ (((mulGrpโ๐) โ Mnd โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก][(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐))) โ ((mulGrpโ๐
) โ Mnd โง [๐ต / ๐][ + / ๐][ ยท / ๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐))))) |
61 | | df-srg 19926 |
. . 3
โข SRing =
{๐ โ CMnd โฃ
((mulGrpโ๐) โ
Mnd โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก][(0gโ๐) / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐)))} |
62 | 60, 61 | elrab2 3652 |
. 2
โข (๐
โ SRing โ (๐
โ CMnd โง
((mulGrpโ๐
) โ
Mnd โง [๐ต / ๐][ + / ๐][ ยท /
๐ก][ 0 / ๐]โ๐ฅ โ ๐ (โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โง ((๐๐ก๐ฅ) = ๐ โง (๐ฅ๐ก๐) = ๐))))) |
63 | | 3anass 1096 |
. 2
โข ((๐
โ CMnd โง ๐บ โ Mnd โง โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 ))) โ (๐
โ CMnd โง (๐บ โ Mnd โง โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 ))))) |
64 | 45, 62, 63 | 3bitr4i 303 |
1
โข (๐
โ SRing โ (๐
โ CMnd โง ๐บ โ Mnd โง โ๐ฅ โ ๐ต (โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) โง (( 0 ยท ๐ฅ) = 0 โง (๐ฅ ยท 0 ) = 0 )))) |