Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©} = {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} |
2 | 1 | grp1 18862 |
. . 3
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} β Grp) |
3 | | snex 5392 |
. . . . . 6
β’ {π} β V |
4 | | ring1.m |
. . . . . . 7
β’ π = {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} |
5 | 4 | rngbase 17188 |
. . . . . 6
β’ ({π} β V β {π} = (Baseβπ)) |
6 | 3, 5 | ax-mp 5 |
. . . . 5
β’ {π} = (Baseβπ) |
7 | 6 | eqcomi 2742 |
. . . 4
β’
(Baseβπ) =
{π} |
8 | | snex 5392 |
. . . . 5
β’
{β¨β¨π,
πβ©, πβ©} β V |
9 | 4 | rngplusg 17189 |
. . . . . 6
β’
({β¨β¨π,
πβ©, πβ©} β V β {β¨β¨π, πβ©, πβ©} = (+gβπ)) |
10 | 9 | eqcomd 2739 |
. . . . 5
β’
({β¨β¨π,
πβ©, πβ©} β V β
(+gβπ) =
{β¨β¨π, πβ©, πβ©}) |
11 | 8, 10 | ax-mp 5 |
. . . 4
β’
(+gβπ) = {β¨β¨π, πβ©, πβ©} |
12 | 7, 11, 1 | grppropstr 18775 |
. . 3
β’ (π β Grp β
{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©} β Grp) |
13 | 2, 12 | sylibr 233 |
. 2
β’ (π β π β π β Grp) |
14 | 1 | mnd1 18605 |
. . 3
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} β Mnd) |
15 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
16 | 15, 6 | mgpbas 19910 |
. . . . 5
β’ {π} =
(Baseβ(mulGrpβπ)) |
17 | 1 | grpbase 17175 |
. . . . . 6
β’ ({π} β V β {π} =
(Baseβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
18 | 3, 17 | ax-mp 5 |
. . . . 5
β’ {π} =
(Baseβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©}) |
19 | 16, 18 | eqtr3i 2763 |
. . . 4
β’
(Baseβ(mulGrpβπ)) = (Baseβ{β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©}) |
20 | 4 | rngmulr 17190 |
. . . . . 6
β’
({β¨β¨π,
πβ©, πβ©} β V β {β¨β¨π, πβ©, πβ©} = (.rβπ)) |
21 | 8, 20 | ax-mp 5 |
. . . . 5
β’
{β¨β¨π,
πβ©, πβ©} = (.rβπ) |
22 | 1 | grpplusg 17177 |
. . . . . 6
β’
({β¨β¨π,
πβ©, πβ©} β V β {β¨β¨π, πβ©, πβ©} =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
23 | 8, 22 | ax-mp 5 |
. . . . 5
β’
{β¨β¨π,
πβ©, πβ©} =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©}) |
24 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
25 | 15, 24 | mgpplusg 19908 |
. . . . 5
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
26 | 21, 23, 25 | 3eqtr3ri 2770 |
. . . 4
β’
(+gβ(mulGrpβπ)) =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©}) |
27 | 19, 26 | mndprop 18590 |
. . 3
β’
((mulGrpβπ)
β Mnd β {β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©} β Mnd) |
28 | 14, 27 | sylibr 233 |
. 2
β’ (π β π β (mulGrpβπ) β Mnd) |
29 | | df-ov 7364 |
. . . . . 6
β’ (π{β¨β¨π, πβ©, πβ©}π) = ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) |
30 | | opex 5425 |
. . . . . . 7
β’
β¨π, πβ© β V |
31 | | fvsng 7130 |
. . . . . . 7
β’
((β¨π, πβ© β V β§ π β π) β ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) = π) |
32 | 30, 31 | mpan 689 |
. . . . . 6
β’ (π β π β ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) = π) |
33 | 29, 32 | eqtrid 2785 |
. . . . 5
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = π) |
34 | 33 | oveq2d 7377 |
. . . 4
β’ (π β π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©}π)) |
35 | 33, 33 | oveq12d 7379 |
. . . 4
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©}π)) |
36 | 34, 35 | eqtr4d 2776 |
. . 3
β’ (π β π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
37 | 33 | oveq1d 7376 |
. . . 4
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
38 | 37, 35 | eqtr4d 2776 |
. . 3
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
39 | | oveq1 7368 |
. . . . . . . 8
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
40 | | oveq1 7368 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
41 | | oveq1 7368 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
42 | 40, 41 | oveq12d 7379 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
43 | 39, 42 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
44 | 40 | oveq1d 7376 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
45 | 41 | oveq1d 7376 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
46 | 44, 45 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
47 | 43, 46 | anbi12d 632 |
. . . . . 6
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
48 | 47 | 2ralbidv 3209 |
. . . . 5
β’ (π = π β (βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
49 | 48 | ralsng 4638 |
. . . 4
β’ (π β π β (βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
50 | | oveq1 7368 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
51 | 50 | oveq2d 7377 |
. . . . . . . 8
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
52 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
53 | 52 | oveq1d 7376 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
54 | 51, 53 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
55 | 52 | oveq1d 7376 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
56 | 50 | oveq2d 7377 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
57 | 55, 56 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
58 | 54, 57 | anbi12d 632 |
. . . . . 6
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
59 | 58 | ralbidv 3171 |
. . . . 5
β’ (π = π β (βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
60 | 59 | ralsng 4638 |
. . . 4
β’ (π β π β (βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
61 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
62 | 61 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
63 | 61 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
64 | 62, 63 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
65 | | oveq2 7369 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
66 | 61, 61 | oveq12d 7379 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
67 | 65, 66 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
68 | 64, 67 | anbi12d 632 |
. . . . 5
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
69 | 68 | ralsng 4638 |
. . . 4
β’ (π β π β (βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
70 | 49, 60, 69 | 3bitrd 305 |
. . 3
β’ (π β π β (βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
71 | 36, 38, 70 | mpbir2and 712 |
. 2
β’ (π β π β βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
72 | 8, 9 | ax-mp 5 |
. . 3
β’
{β¨β¨π,
πβ©, πβ©} = (+gβπ) |
73 | 6, 15, 72, 21 | isring 19976 |
. 2
β’ (π β Ring β (π β Grp β§
(mulGrpβπ) β Mnd
β§ βπ β
{π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
74 | 13, 28, 71, 73 | syl3anbrc 1344 |
1
β’ (π β π β π β Ring) |