Step | Hyp | Ref
| Expression |
1 | | fveq2 6889 |
. . . . . 6
โข (๐ = ๐
โ (mulGrpโ๐) = (mulGrpโ๐
)) |
2 | | isrng.g |
. . . . . 6
โข ๐บ = (mulGrpโ๐
) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
โข (๐ = ๐
โ (mulGrpโ๐) = ๐บ) |
4 | 3 | eleq1d 2819 |
. . . 4
โข (๐ = ๐
โ ((mulGrpโ๐) โ Smgrp โ ๐บ โ Smgrp)) |
5 | | fvexd 6904 |
. . . . 5
โข (๐ = ๐
โ (Baseโ๐) โ V) |
6 | | fveq2 6889 |
. . . . . 6
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
7 | | isrng.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
8 | 6, 7 | eqtr4di 2791 |
. . . . 5
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
9 | | fvexd 6904 |
. . . . . 6
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) โ V) |
10 | | fveq2 6889 |
. . . . . . . 8
โข (๐ = ๐
โ (+gโ๐) = (+gโ๐
)) |
11 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) = (+gโ๐
)) |
12 | | isrng.p |
. . . . . . 7
โข + =
(+gโ๐
) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . 6
โข ((๐ = ๐
โง ๐ = ๐ต) โ (+gโ๐) = + ) |
14 | | fvexd 6904 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐)
โ V) |
15 | | fveq2 6889 |
. . . . . . . . . 10
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
16 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐ต) โ (.rโ๐) = (.rโ๐
)) |
17 | 16 | adantr 482 |
. . . . . . . 8
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐) =
(.rโ๐
)) |
18 | | isrng.t |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
(.rโ๐) =
ยท
) |
20 | | simpllr 775 |
. . . . . . . 8
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ = ๐ต) |
21 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ก = ยท ) |
22 | | eqidd 2734 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ฅ = ๐ฅ) |
23 | | oveq 7412 |
. . . . . . . . . . . . . 14
โข (๐ = + โ (๐ฆ๐๐ง) = (๐ฆ + ๐ง)) |
24 | 23 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฆ๐๐ง) = (๐ฆ + ๐ง)) |
25 | 21, 22, 24 | oveq123d 7427 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก(๐ฆ๐๐ง)) = (๐ฅ ยท (๐ฆ + ๐ง))) |
26 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ ๐ = + ) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ = + ) |
28 | | oveq 7412 |
. . . . . . . . . . . . . 14
โข (๐ก = ยท โ (๐ฅ๐ก๐ฆ) = (๐ฅ ยท ๐ฆ)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก๐ฆ) = (๐ฅ ยท ๐ฆ)) |
30 | | oveq 7412 |
. . . . . . . . . . . . . 14
โข (๐ก = ยท โ (๐ฅ๐ก๐ง) = (๐ฅ ยท ๐ง)) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐ก๐ง) = (๐ฅ ยท ๐ง)) |
32 | 27, 29, 31 | oveq123d 7427 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
33 | 25, 32 | eqeq12d 2749 |
. . . . . . . . . . 11
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
34 | | oveq 7412 |
. . . . . . . . . . . . . 14
โข (๐ = + โ (๐ฅ๐๐ฆ) = (๐ฅ + ๐ฆ)) |
35 | 34 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฅ๐๐ฆ) = (๐ฅ + ๐ฆ)) |
36 | | eqidd 2734 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ๐ง = ๐ง) |
37 | 21, 35, 36 | oveq123d 7427 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ + ๐ฆ) ยท ๐ง)) |
38 | | oveq 7412 |
. . . . . . . . . . . . . 14
โข (๐ก = ยท โ (๐ฆ๐ก๐ง) = (๐ฆ ยท ๐ง)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (๐ฆ๐ก๐ง) = (๐ฆ ยท ๐ง)) |
40 | 27, 31, 39 | oveq123d 7427 |
. . . . . . . . . . . 12
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
41 | 37, 40 | eqeq12d 2749 |
. . . . . . . . . . 11
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
42 | 33, 41 | anbi12d 632 |
. . . . . . . . . 10
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ (((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
43 | 20, 42 | raleqbidv 3343 |
. . . . . . . . 9
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
44 | 20, 43 | raleqbidv 3343 |
. . . . . . . 8
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
45 | 20, 44 | raleqbidv 3343 |
. . . . . . 7
โข ((((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โง ๐ก = ยท ) โ
(โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
46 | 14, 19, 45 | sbcied2 3824 |
. . . . . 6
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ = + ) โ
([(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
47 | 9, 13, 46 | sbcied2 3824 |
. . . . 5
โข ((๐ = ๐
โง ๐ = ๐ต) โ ([(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
48 | 5, 8, 47 | sbcied2 3824 |
. . . 4
โข (๐ = ๐
โ ([(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |
49 | 4, 48 | anbi12d 632 |
. . 3
โข (๐ = ๐
โ (((mulGrpโ๐) โ Smgrp โง
[(Baseโ๐) /
๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง)))) โ (๐บ โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
50 | | df-rng 46636 |
. . 3
โข Rng =
{๐ โ Abel โฃ
((mulGrpโ๐) โ
Smgrp โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))))} |
51 | 49, 50 | elrab2 3686 |
. 2
โข (๐
โ Rng โ (๐
โ Abel โง (๐บ โ Smgrp โง
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
52 | | 3anass 1096 |
. 2
โข ((๐
โ Abel โง ๐บ โ Smgrp โง
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) โ (๐
โ Abel โง (๐บ โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))))) |
53 | 51, 52 | bitr4i 278 |
1
โข (๐
โ Rng โ (๐
โ Abel โง ๐บ โ Smgrp โง
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) |