Step | Hyp | Ref
| Expression |
1 | | snexg 4184 |
. . . . . . . 8
β’ (π β π β {π} β V) |
2 | | opexg 4228 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β β¨π, πβ© β V) |
3 | 2 | anidms 397 |
. . . . . . . . . 10
β’ (π β π β β¨π, πβ© β V) |
4 | | opexg 4228 |
. . . . . . . . . 10
β’
((β¨π, πβ© β V β§ π β π) β β¨β¨π, πβ©, πβ© β V) |
5 | 3, 4 | mpancom 422 |
. . . . . . . . 9
β’ (π β π β β¨β¨π, πβ©, πβ© β V) |
6 | | snexg 4184 |
. . . . . . . . 9
β’
(β¨β¨π,
πβ©, πβ© β V β {β¨β¨π, πβ©, πβ©} β V) |
7 | 5, 6 | syl 14 |
. . . . . . . 8
β’ (π β π β {β¨β¨π, πβ©, πβ©} β V) |
8 | | ring1.m |
. . . . . . . . 9
β’ π = {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} |
9 | 8 | rngbaseg 12593 |
. . . . . . . 8
β’ (({π} β V β§
{β¨β¨π, πβ©, πβ©} β V β§ {β¨β¨π, πβ©, πβ©} β V) β {π} = (Baseβπ)) |
10 | 1, 7, 7, 9 | syl3anc 1238 |
. . . . . . 7
β’ (π β π β {π} = (Baseβπ)) |
11 | 10 | opeq2d 3785 |
. . . . . 6
β’ (π β π β β¨(Baseβndx), {π}β© =
β¨(Baseβndx), (Baseβπ)β©) |
12 | 8 | rngplusgg 12594 |
. . . . . . . 8
β’ (({π} β V β§
{β¨β¨π, πβ©, πβ©} β V β§ {β¨β¨π, πβ©, πβ©} β V) β {β¨β¨π, πβ©, πβ©} = (+gβπ)) |
13 | 1, 7, 7, 12 | syl3anc 1238 |
. . . . . . 7
β’ (π β π β {β¨β¨π, πβ©, πβ©} = (+gβπ)) |
14 | 13 | opeq2d 3785 |
. . . . . 6
β’ (π β π β β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β© =
β¨(+gβndx), (+gβπ)β©) |
15 | 11, 14 | preq12d 3677 |
. . . . 5
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} = {β¨(Baseβndx),
(Baseβπ)β©,
β¨(+gβndx), (+gβπ)β©}) |
16 | | eqid 2177 |
. . . . . 6
β’
{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©} = {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} |
17 | 16 | grp1 12975 |
. . . . 5
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} β Grp) |
18 | 15, 17 | eqeltrrd 2255 |
. . . 4
β’ (π β π β {β¨(Baseβndx),
(Baseβπ)β©,
β¨(+gβndx), (+gβπ)β©} β Grp) |
19 | | basendxnn 12517 |
. . . . . . . 8
β’
(Baseβndx) β β |
20 | | opexg 4228 |
. . . . . . . 8
β’
(((Baseβndx) β β β§ {π} β V) β β¨(Baseβndx),
{π}β© β
V) |
21 | 19, 1, 20 | sylancr 414 |
. . . . . . 7
β’ (π β π β β¨(Baseβndx), {π}β© β
V) |
22 | | plusgslid 12570 |
. . . . . . . . 9
β’
(+g = Slot (+gβndx) β§
(+gβndx) β β) |
23 | 22 | simpri 113 |
. . . . . . . 8
β’
(+gβndx) β β |
24 | | opexg 4228 |
. . . . . . . 8
β’
(((+gβndx) β β β§ {β¨β¨π, πβ©, πβ©} β V) β
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β© β V) |
25 | 23, 7, 24 | sylancr 414 |
. . . . . . 7
β’ (π β π β β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β© β V) |
26 | | mulrslid 12589 |
. . . . . . . . 9
β’
(.r = Slot (.rβndx) β§
(.rβndx) β β) |
27 | 26 | simpri 113 |
. . . . . . . 8
β’
(.rβndx) β β |
28 | | opexg 4228 |
. . . . . . . 8
β’
(((.rβndx) β β β§ {β¨β¨π, πβ©, πβ©} β V) β
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β© β V) |
29 | 27, 7, 28 | sylancr 414 |
. . . . . . 7
β’ (π β π β β¨(.rβndx),
{β¨β¨π, πβ©, πβ©}β© β V) |
30 | | tpexg 4444 |
. . . . . . 7
β’
((β¨(Baseβndx), {π}β© β V β§
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β© β V β§
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β© β V) β
{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β V) |
31 | 21, 25, 29, 30 | syl3anc 1238 |
. . . . . 6
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β V) |
32 | 8, 31 | eqeltrid 2264 |
. . . . 5
β’ (π β π β π β V) |
33 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
34 | | eqid 2177 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
35 | | eqid 2177 |
. . . . . 6
β’
{β¨(Baseβndx), (Baseβπ)β©, β¨(+gβndx),
(+gβπ)β©} = {β¨(Baseβndx),
(Baseβπ)β©,
β¨(+gβndx), (+gβπ)β©} |
36 | 33, 34, 35 | grppropstrg 12894 |
. . . . 5
β’ (π β V β (π β Grp β
{β¨(Baseβndx), (Baseβπ)β©, β¨(+gβndx),
(+gβπ)β©} β Grp)) |
37 | 32, 36 | syl 14 |
. . . 4
β’ (π β π β (π β Grp β {β¨(Baseβndx),
(Baseβπ)β©,
β¨(+gβndx), (+gβπ)β©} β Grp)) |
38 | 18, 37 | mpbird 167 |
. . 3
β’ (π β π β π β Grp) |
39 | 16 | mnd1 12846 |
. . . 4
β’ (π β π β {β¨(Baseβndx), {π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} β Mnd) |
40 | | eqidd 2178 |
. . . . 5
β’ (π β π β (Baseβ(mulGrpβπ)) =
(Baseβ(mulGrpβπ))) |
41 | 16 | grpbaseg 12584 |
. . . . . . 7
β’ (({π} β V β§
{β¨β¨π, πβ©, πβ©} β V) β {π} = (Baseβ{β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©})) |
42 | 1, 7, 41 | syl2anc 411 |
. . . . . 6
β’ (π β π β {π} = (Baseβ{β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©})) |
43 | | eqid 2177 |
. . . . . . . 8
β’
(mulGrpβπ) =
(mulGrpβπ) |
44 | 43, 33 | mgpbasg 13134 |
. . . . . . 7
β’ (π β V β
(Baseβπ) =
(Baseβ(mulGrpβπ))) |
45 | 32, 44 | syl 14 |
. . . . . 6
β’ (π β π β (Baseβπ) = (Baseβ(mulGrpβπ))) |
46 | 10, 42, 45 | 3eqtr3rd 2219 |
. . . . 5
β’ (π β π β (Baseβ(mulGrpβπ)) =
(Baseβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
47 | 8 | rngmulrg 12595 |
. . . . . . . 8
β’ (({π} β V β§
{β¨β¨π, πβ©, πβ©} β V β§ {β¨β¨π, πβ©, πβ©} β V) β {β¨β¨π, πβ©, πβ©} = (.rβπ)) |
48 | 1, 7, 7, 47 | syl3anc 1238 |
. . . . . . 7
β’ (π β π β {β¨β¨π, πβ©, πβ©} = (.rβπ)) |
49 | 16 | grpplusgg 12585 |
. . . . . . . 8
β’ (({π} β V β§
{β¨β¨π, πβ©, πβ©} β V) β {β¨β¨π, πβ©, πβ©} =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
50 | 1, 7, 49 | syl2anc 411 |
. . . . . . 7
β’ (π β π β {β¨β¨π, πβ©, πβ©} =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
51 | | eqid 2177 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
52 | 43, 51 | mgpplusgg 13132 |
. . . . . . . 8
β’ (π β V β
(.rβπ) =
(+gβ(mulGrpβπ))) |
53 | 32, 52 | syl 14 |
. . . . . . 7
β’ (π β π β (.rβπ) =
(+gβ(mulGrpβπ))) |
54 | 48, 50, 53 | 3eqtr3rd 2219 |
. . . . . 6
β’ (π β π β
(+gβ(mulGrpβπ)) =
(+gβ{β¨(Baseβndx), {π}β©, β¨(+gβndx),
{β¨β¨π, πβ©, πβ©}β©})) |
55 | 54 | oveqdr 5902 |
. . . . 5
β’ ((π β π β§ (π₯ β (Baseβ(mulGrpβπ)) β§ π¦ β (Baseβ(mulGrpβπ)))) β (π₯(+gβ(mulGrpβπ))π¦) = (π₯(+gβ{β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©})π¦)) |
56 | 40, 46, 55 | mndpropd 12840 |
. . . 4
β’ (π β π β ((mulGrpβπ) β Mnd β {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©} β Mnd)) |
57 | 39, 56 | mpbird 167 |
. . 3
β’ (π β π β (mulGrpβπ) β Mnd) |
58 | | df-ov 5877 |
. . . . . . 7
β’ (π{β¨β¨π, πβ©, πβ©}π) = ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) |
59 | | fvsng 5712 |
. . . . . . . 8
β’
((β¨π, πβ© β V β§ π β π) β ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) = π) |
60 | 3, 59 | mpancom 422 |
. . . . . . 7
β’ (π β π β ({β¨β¨π, πβ©, πβ©}ββ¨π, πβ©) = π) |
61 | 58, 60 | eqtrid 2222 |
. . . . . 6
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = π) |
62 | 61 | oveq2d 5890 |
. . . . 5
β’ (π β π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©}π)) |
63 | 61, 61 | oveq12d 5892 |
. . . . 5
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©}π)) |
64 | 62, 63 | eqtr4d 2213 |
. . . 4
β’ (π β π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
65 | 61 | oveq1d 5889 |
. . . . 5
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
66 | 65, 63 | eqtr4d 2213 |
. . . 4
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
67 | | oveq1 5881 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
68 | | oveq1 5881 |
. . . . . . . . . 10
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
69 | | oveq1 5881 |
. . . . . . . . . 10
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
70 | 68, 69 | oveq12d 5892 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
71 | 67, 70 | eqeq12d 2192 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
72 | 68 | oveq1d 5889 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
73 | 69 | oveq1d 5889 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
74 | 72, 73 | eqeq12d 2192 |
. . . . . . . 8
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
75 | 71, 74 | anbi12d 473 |
. . . . . . 7
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
76 | 75 | 2ralbidv 2501 |
. . . . . 6
β’ (π = π β (βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
77 | 76 | ralsng 3632 |
. . . . 5
β’ (π β π β (βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
78 | | oveq1 5881 |
. . . . . . . . . 10
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
79 | 78 | oveq2d 5890 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
80 | | oveq2 5882 |
. . . . . . . . . 10
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
81 | 80 | oveq1d 5889 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
82 | 79, 81 | eqeq12d 2192 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
83 | 80 | oveq1d 5889 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
84 | 78 | oveq2d 5890 |
. . . . . . . . 9
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
85 | 83, 84 | eqeq12d 2192 |
. . . . . . . 8
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
86 | 82, 85 | anbi12d 473 |
. . . . . . 7
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
87 | 86 | ralbidv 2477 |
. . . . . 6
β’ (π = π β (βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
88 | 87 | ralsng 3632 |
. . . . 5
β’ (π β π β (βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
89 | | oveq2 5882 |
. . . . . . . . 9
β’ (π = π β (π{β¨β¨π, πβ©, πβ©}π) = (π{β¨β¨π, πβ©, πβ©}π)) |
90 | 89 | oveq2d 5890 |
. . . . . . . 8
β’ (π = π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
91 | 89 | oveq2d 5890 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
92 | 90, 91 | eqeq12d 2192 |
. . . . . . 7
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
93 | | oveq2 5882 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π)) |
94 | 89, 89 | oveq12d 5892 |
. . . . . . . 8
β’ (π = π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) |
95 | 93, 94 | eqeq12d 2192 |
. . . . . . 7
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
96 | 92, 95 | anbi12d 473 |
. . . . . 6
β’ (π = π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
97 | 96 | ralsng 3632 |
. . . . 5
β’ (π β π β (βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
98 | 77, 88, 97 | 3bitrd 214 |
. . . 4
β’ (π β π β (βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
99 | 64, 66, 98 | mpbir2and 944 |
. . 3
β’ (π β π β βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) |
100 | 38, 57, 99 | 3jca 1177 |
. 2
β’ (π β π β (π β Grp β§ (mulGrpβπ) β Mnd β§ βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))))) |
101 | | eqidd 2178 |
. . . . . . . . . 10
β’ (π β π β π = π) |
102 | 13 | oveqd 5891 |
. . . . . . . . . 10
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = (π(+gβπ)π)) |
103 | 48, 101, 102 | oveq123d 5895 |
. . . . . . . . 9
β’ (π β π β (π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = (π(.rβπ)(π(+gβπ)π))) |
104 | 48 | oveqd 5891 |
. . . . . . . . . 10
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = (π(.rβπ)π)) |
105 | 48 | oveqd 5891 |
. . . . . . . . . 10
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = (π(.rβπ)π)) |
106 | 13, 104, 105 | oveq123d 5895 |
. . . . . . . . 9
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))) |
107 | 103, 106 | eqeq12d 2192 |
. . . . . . . 8
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β (π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)))) |
108 | 13 | oveqd 5891 |
. . . . . . . . . 10
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = (π(+gβπ)π)) |
109 | | eqidd 2178 |
. . . . . . . . . 10
β’ (π β π β π = π) |
110 | 48, 108, 109 | oveq123d 5895 |
. . . . . . . . 9
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π(+gβπ)π)(.rβπ)π)) |
111 | 48 | oveqd 5891 |
. . . . . . . . . 10
β’ (π β π β (π{β¨β¨π, πβ©, πβ©}π) = (π(.rβπ)π)) |
112 | 13, 105, 111 | oveq123d 5895 |
. . . . . . . . 9
β’ (π β π β ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))) |
113 | 110, 112 | eqeq12d 2192 |
. . . . . . . 8
β’ (π β π β (((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)))) |
114 | 107, 113 | anbi12d 473 |
. . . . . . 7
β’ (π β π β (((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β ((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))))) |
115 | 10, 114 | raleqbidv 2684 |
. . . . . 6
β’ (π β π β (βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β (Baseβπ)((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))))) |
116 | 10, 115 | raleqbidv 2684 |
. . . . 5
β’ (π β π β (βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β (Baseβπ)βπ β (Baseβπ)((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))))) |
117 | 10, 116 | raleqbidv 2684 |
. . . 4
β’ (π β π β (βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π))) β βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))))) |
118 | 117 | 3anbi3d 1318 |
. . 3
β’ (π β π β ((π β Grp β§ (mulGrpβπ) β Mnd β§ βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) β (π β Grp β§ (mulGrpβπ) β Mnd β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)))))) |
119 | 33, 43, 34, 51 | isring 13181 |
. . 3
β’ (π β Ring β (π β Grp β§
(mulGrpβπ) β Mnd
β§ βπ β
(Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)((π(.rβπ)(π(+gβπ)π)) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π)) β§ ((π(+gβπ)π)(.rβπ)π) = ((π(.rβπ)π)(+gβπ)(π(.rβπ)π))))) |
120 | 118, 119 | bitr4di 198 |
. 2
β’ (π β π β ((π β Grp β§ (mulGrpβπ) β Mnd β§ βπ β {π}βπ β {π}βπ β {π} ((π{β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)) β§ ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©}π) = ((π{β¨β¨π, πβ©, πβ©}π){β¨β¨π, πβ©, πβ©} (π{β¨β¨π, πβ©, πβ©}π)))) β π β Ring)) |
121 | 100, 120 | mpbid 147 |
1
β’ (π β π β π β Ring) |