Step |
Hyp |
Ref |
Expression |
1 |
|
islmod.v |
โข ๐ = ( Base โ ๐ ) |
2 |
|
islmod.a |
โข + = ( +g โ ๐ ) |
3 |
|
islmod.s |
โข ยท = ( ยท๐ โ ๐ ) |
4 |
|
islmod.f |
โข ๐น = ( Scalar โ ๐ ) |
5 |
|
islmod.k |
โข ๐พ = ( Base โ ๐น ) |
6 |
|
islmod.p |
โข โจฃ = ( +g โ ๐น ) |
7 |
|
islmod.t |
โข ร = ( .r โ ๐น ) |
8 |
|
islmod.u |
โข 1 = ( 1r โ ๐น ) |
9 |
|
fveq2 |
โข ( ๐ = ๐ โ ( Base โ ๐ ) = ( Base โ ๐ ) ) |
10 |
9 1
|
eqtr4di |
โข ( ๐ = ๐ โ ( Base โ ๐ ) = ๐ ) |
11 |
|
fveq2 |
โข ( ๐ = ๐ โ ( +g โ ๐ ) = ( +g โ ๐ ) ) |
12 |
11 2
|
eqtr4di |
โข ( ๐ = ๐ โ ( +g โ ๐ ) = + ) |
13 |
|
fveq2 |
โข ( ๐ = ๐ โ ( Scalar โ ๐ ) = ( Scalar โ ๐ ) ) |
14 |
13 4
|
eqtr4di |
โข ( ๐ = ๐ โ ( Scalar โ ๐ ) = ๐น ) |
15 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) ) |
16 |
15 3
|
eqtr4di |
โข ( ๐ = ๐ โ ( ยท๐ โ ๐ ) = ยท ) |
17 |
16
|
sbceq1d |
โข ( ๐ = ๐ โ ( [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
18 |
14 17
|
sbceqbid |
โข ( ๐ = ๐ โ ( [ ( Scalar โ ๐ ) / ๐ ] [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ๐น / ๐ ] [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
19 |
12 18
|
sbceqbid |
โข ( ๐ = ๐ โ ( [ ( +g โ ๐ ) / ๐ ] [ ( Scalar โ ๐ ) / ๐ ] [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ + / ๐ ] [ ๐น / ๐ ] [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
20 |
10 19
|
sbceqbid |
โข ( ๐ = ๐ โ ( [ ( Base โ ๐ ) / ๐ฃ ] [ ( +g โ ๐ ) / ๐ ] [ ( Scalar โ ๐ ) / ๐ ] [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ๐ / ๐ฃ ] [ + / ๐ ] [ ๐น / ๐ ] [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
21 |
1
|
fvexi |
โข ๐ โ V |
22 |
2
|
fvexi |
โข + โ V |
23 |
4
|
fvexi |
โข ๐น โ V |
24 |
|
simp3 |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ๐ = ๐น ) |
25 |
24
|
fveq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( Base โ ๐ ) = ( Base โ ๐น ) ) |
26 |
25 5
|
eqtr4di |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( Base โ ๐ ) = ๐พ ) |
27 |
24
|
fveq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( +g โ ๐ ) = ( +g โ ๐น ) ) |
28 |
27 6
|
eqtr4di |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( +g โ ๐ ) = โจฃ ) |
29 |
24
|
fveq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( .r โ ๐ ) = ( .r โ ๐น ) ) |
30 |
29 7
|
eqtr4di |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( .r โ ๐ ) = ร ) |
31 |
30
|
sbceq1d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ร / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
32 |
7
|
fvexi |
โข ร โ V |
33 |
|
oveq |
โข ( ๐ก = ร โ ( ๐ ๐ก ๐ ) = ( ๐ ร ๐ ) ) |
34 |
33
|
oveq1d |
โข ( ๐ก = ร โ ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ( ๐ ร ๐ ) ๐ ๐ค ) ) |
35 |
34
|
eqeq1d |
โข ( ๐ก = ร โ ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โ ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) ) ) |
36 |
35
|
anbi1d |
โข ( ๐ก = ร โ ( ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) โ ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) |
37 |
36
|
anbi2d |
โข ( ๐ก = ร โ ( ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) |
38 |
37
|
2ralbidv |
โข ( ๐ก = ร โ ( โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) |
39 |
38
|
2ralbidv |
โข ( ๐ก = ร โ ( โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) |
40 |
39
|
anbi2d |
โข ( ๐ก = ร โ ( ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) ) |
41 |
32 40
|
sbcie |
โข ( [ ร / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) ) |
42 |
24
|
eleq1d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ๐ โ Ring โ ๐น โ Ring ) ) |
43 |
|
simp1 |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ๐ฃ = ๐ ) |
44 |
43
|
eleq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ๐ ๐ ๐ค ) โ ๐ฃ โ ( ๐ ๐ ๐ค ) โ ๐ ) ) |
45 |
|
simp2 |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ๐ = + ) |
46 |
45
|
oveqd |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ๐ค ๐ ๐ฅ ) = ( ๐ค + ๐ฅ ) ) |
47 |
46
|
oveq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ๐ ๐ ( ๐ค + ๐ฅ ) ) ) |
48 |
45
|
oveqd |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) ) |
49 |
47 48
|
eqeq12d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โ ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) ) ) |
50 |
45
|
oveqd |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) |
51 |
50
|
eqeq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) โ ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) ) |
52 |
44 49 51
|
3anbi123d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โ ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) ) ) |
53 |
24
|
fveq2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( 1r โ ๐ ) = ( 1r โ ๐น ) ) |
54 |
53 8
|
eqtr4di |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( 1r โ ๐ ) = 1 ) |
55 |
54
|
oveq1d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( 1r โ ๐ ) ๐ ๐ค ) = ( 1 ๐ ๐ค ) ) |
56 |
55
|
eqeq1d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค โ ( 1 ๐ ๐ค ) = ๐ค ) ) |
57 |
56
|
anbi2d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) โ ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) |
58 |
52 57
|
anbi12d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) |
59 |
43 58
|
raleqbidv |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) |
60 |
43 59
|
raleqbidv |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) |
61 |
60
|
2ralbidv |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) โ โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) |
62 |
42 61
|
anbi12d |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
63 |
41 62
|
bitrid |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ร / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
64 |
31 63
|
bitrd |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
65 |
28 64
|
sbceqbid |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ โจฃ / ๐ ] ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
66 |
26 65
|
sbceqbid |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ๐พ / ๐ ] [ โจฃ / ๐ ] ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
67 |
66
|
sbcbidv |
โข ( ( ๐ฃ = ๐ โง ๐ = + โง ๐ = ๐น ) โ ( [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ยท / ๐ ] [ ๐พ / ๐ ] [ โจฃ / ๐ ] ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) ) |
68 |
21 22 23 67
|
sbc3ie |
โข ( [ ๐ / ๐ฃ ] [ + / ๐ ] [ ๐น / ๐ ] [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ [ ยท / ๐ ] [ ๐พ / ๐ ] [ โจฃ / ๐ ] ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) ) |
69 |
3
|
fvexi |
โข ยท โ V |
70 |
5
|
fvexi |
โข ๐พ โ V |
71 |
6
|
fvexi |
โข โจฃ โ V |
72 |
|
simp2 |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ๐ = ๐พ ) |
73 |
|
simp1 |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ๐ = ยท ) |
74 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ๐ค ) = ( ๐ ยท ๐ค ) ) |
75 |
74
|
eleq1d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ๐ค ) โ ๐ โ ( ๐ ยท ๐ค ) โ ๐ ) ) |
76 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ๐ ยท ( ๐ค + ๐ฅ ) ) ) |
77 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ๐ฅ ) = ( ๐ ยท ๐ฅ ) ) |
78 |
74 77
|
oveq12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) ) |
79 |
76 78
|
eqeq12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โ ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) ) ) |
80 |
|
simp3 |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ๐ = โจฃ ) |
81 |
80
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ๐ ) = ( ๐ โจฃ ๐ ) ) |
82 |
81
|
oveq1d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ โจฃ ๐ ) ๐ ๐ค ) ) |
83 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ โจฃ ๐ ) ๐ ๐ค ) = ( ( ๐ โจฃ ๐ ) ยท ๐ค ) ) |
84 |
82 83
|
eqtrd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ โจฃ ๐ ) ยท ๐ค ) ) |
85 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ๐ค ) = ( ๐ ยท ๐ค ) ) |
86 |
85 74
|
oveq12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) |
87 |
84 86
|
eqeq12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) โ ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) ) |
88 |
75 79 87
|
3anbi123d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โ ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) ) ) |
89 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ( ๐ ร ๐ ) ยท ๐ค ) ) |
90 |
74
|
oveq2d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ( ๐ ๐ ๐ค ) ) = ( ๐ ๐ ( ๐ ยท ๐ค ) ) ) |
91 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ( ๐ ยท ๐ค ) ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) ) |
92 |
90 91
|
eqtrd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ๐ ๐ ( ๐ ๐ ๐ค ) ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) ) |
93 |
89 92
|
eqeq12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โ ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) ) ) |
94 |
73
|
oveqd |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( 1 ๐ ๐ค ) = ( 1 ยท ๐ค ) ) |
95 |
94
|
eqeq1d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( 1 ๐ ๐ค ) = ๐ค โ ( 1 ยท ๐ค ) = ๐ค ) ) |
96 |
93 95
|
anbi12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) โ ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) |
97 |
88 96
|
anbi12d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) โ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
98 |
97
|
2ralbidv |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) โ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
99 |
72 98
|
raleqbidv |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) โ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
100 |
72 99
|
raleqbidv |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) โ โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
101 |
100
|
anbi2d |
โข ( ( ๐ = ยท โง ๐ = ๐พ โง ๐ = โจฃ ) โ ( ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) ) |
102 |
69 70 71 101
|
sbc3ie |
โข ( [ ยท / ๐ ] [ ๐พ / ๐ ] [ โจฃ / ๐ ] ( ๐น โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ๐ ๐ค ) โ ๐ โง ( ๐ ๐ ( ๐ค + ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) + ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( 1 ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
103 |
68 102
|
bitri |
โข ( [ ๐ / ๐ฃ ] [ + / ๐ ] [ ๐น / ๐ ] [ ยท / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |
104 |
20 103
|
bitrdi |
โข ( ๐ = ๐ โ ( [ ( Base โ ๐ ) / ๐ฃ ] [ ( +g โ ๐ ) / ๐ ] [ ( Scalar โ ๐ ) / ๐ ] [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) โ ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) ) |
105 |
|
df-lmod |
โข LMod = { ๐ โ Grp โฃ [ ( Base โ ๐ ) / ๐ฃ ] [ ( +g โ ๐ ) / ๐ ] [ ( Scalar โ ๐ ) / ๐ ] [ ( ยท๐ โ ๐ ) / ๐ ] [ ( Base โ ๐ ) / ๐ ] [ ( +g โ ๐ ) / ๐ ] [ ( .r โ ๐ ) / ๐ก ] ( ๐ โ Ring โง โ ๐ โ ๐ โ ๐ โ ๐ โ ๐ฅ โ ๐ฃ โ ๐ค โ ๐ฃ ( ( ( ๐ ๐ ๐ค ) โ ๐ฃ โง ( ๐ ๐ ( ๐ค ๐ ๐ฅ ) ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ฅ ) ) โง ( ( ๐ ๐ ๐ ) ๐ ๐ค ) = ( ( ๐ ๐ ๐ค ) ๐ ( ๐ ๐ ๐ค ) ) ) โง ( ( ( ๐ ๐ก ๐ ) ๐ ๐ค ) = ( ๐ ๐ ( ๐ ๐ ๐ค ) ) โง ( ( 1r โ ๐ ) ๐ ๐ค ) = ๐ค ) ) ) } |
106 |
104 105
|
elrab2 |
โข ( ๐ โ LMod โ ( ๐ โ Grp โง ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) ) |
107 |
|
3anass |
โข ( ( ๐ โ Grp โง ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) โ ( ๐ โ Grp โง ( ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) ) |
108 |
106 107
|
bitr4i |
โข ( ๐ โ LMod โ ( ๐ โ Grp โง ๐น โ Ring โง โ ๐ โ ๐พ โ ๐ โ ๐พ โ ๐ฅ โ ๐ โ ๐ค โ ๐ ( ( ( ๐ ยท ๐ค ) โ ๐ โง ( ๐ ยท ( ๐ค + ๐ฅ ) ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ฅ ) ) โง ( ( ๐ โจฃ ๐ ) ยท ๐ค ) = ( ( ๐ ยท ๐ค ) + ( ๐ ยท ๐ค ) ) ) โง ( ( ( ๐ ร ๐ ) ยท ๐ค ) = ( ๐ ยท ( ๐ ยท ๐ค ) ) โง ( 1 ยท ๐ค ) = ๐ค ) ) ) ) |