Step | Hyp | Ref
| Expression |
1 | | mgpress.2 |
. . 3
β’ π = (mulGrpβπ
) |
2 | | simpr 486 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β (Baseβπ
) β π΄) |
3 | 1 | fvexi 6861 |
. . . . 5
β’ π β V |
4 | 3 | a1i 11 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β π β V) |
5 | | simplr 768 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β π΄ β π) |
6 | | eqid 2737 |
. . . . 5
β’ (π βΎs π΄) = (π βΎs π΄) |
7 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
8 | 1, 7 | mgpbas 19909 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ) |
9 | 6, 8 | ressid2 17123 |
. . . 4
β’
(((Baseβπ
)
β π΄ β§ π β V β§ π΄ β π) β (π βΎs π΄) = π) |
10 | 2, 4, 5, 9 | syl3anc 1372 |
. . 3
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β (π βΎs π΄) = π) |
11 | | simpll 766 |
. . . . 5
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β π
β π) |
12 | | mgpress.1 |
. . . . . 6
β’ π = (π
βΎs π΄) |
13 | 12, 7 | ressid2 17123 |
. . . . 5
β’
(((Baseβπ
)
β π΄ β§ π
β π β§ π΄ β π) β π = π
) |
14 | 2, 11, 5, 13 | syl3anc 1372 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β π = π
) |
15 | 14 | fveq2d 6851 |
. . 3
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β (mulGrpβπ) = (mulGrpβπ
)) |
16 | 1, 10, 15 | 3eqtr4a 2803 |
. 2
β’ (((π
β π β§ π΄ β π) β§ (Baseβπ
) β π΄) β (π βΎs π΄) = (mulGrpβπ)) |
17 | | eqid 2737 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
18 | 1, 17 | mgpval 19906 |
. . . 4
β’ π = (π
sSet β¨(+gβndx),
(.rβπ
)β©) |
19 | 18 | oveq1i 7372 |
. . 3
β’ (π sSet β¨(Baseβndx),
(π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) |
20 | | simpr 486 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β Β¬ (Baseβπ
) β π΄) |
21 | 3 | a1i 11 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β π β V) |
22 | | simplr 768 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β π΄ β π) |
23 | 6, 8 | ressval2 17124 |
. . . 4
β’ ((Β¬
(Baseβπ
) β
π΄ β§ π β V β§ π΄ β π) β (π βΎs π΄) = (π sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
24 | 20, 21, 22, 23 | syl3anc 1372 |
. . 3
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (π βΎs π΄) = (π sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
25 | | eqid 2737 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
26 | | eqid 2737 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
27 | 25, 26 | mgpval 19906 |
. . . . 5
β’
(mulGrpβπ) =
(π sSet
β¨(+gβndx), (.rβπ)β©) |
28 | | simpll 766 |
. . . . . . 7
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β π
β π) |
29 | 12, 7 | ressval2 17124 |
. . . . . . 7
β’ ((Β¬
(Baseβπ
) β
π΄ β§ π
β π β§ π΄ β π) β π = (π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
30 | 20, 28, 22, 29 | syl3anc 1372 |
. . . . . 6
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β π = (π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
31 | 12, 17 | ressmulr 17195 |
. . . . . . . . 9
β’ (π΄ β π β (.rβπ
) = (.rβπ)) |
32 | 31 | eqcomd 2743 |
. . . . . . . 8
β’ (π΄ β π β (.rβπ) = (.rβπ
)) |
33 | 32 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (.rβπ) = (.rβπ
)) |
34 | 33 | opeq2d 4842 |
. . . . . 6
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β β¨(+gβndx),
(.rβπ)β© = β¨(+gβndx),
(.rβπ
)β©) |
35 | 30, 34 | oveq12d 7380 |
. . . . 5
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (π sSet β¨(+gβndx),
(.rβπ)β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
36 | 27, 35 | eqtrid 2789 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (mulGrpβπ) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
37 | | 1ne2 12368 |
. . . . . . 7
β’ 1 β
2 |
38 | 37 | necomi 2999 |
. . . . . 6
β’ 2 β
1 |
39 | | plusgndx 17166 |
. . . . . . 7
β’
(+gβndx) = 2 |
40 | | basendx 17099 |
. . . . . . 7
β’
(Baseβndx) = 1 |
41 | 39, 40 | neeq12i 3011 |
. . . . . 6
β’
((+gβndx) β (Baseβndx) β 2 β
1) |
42 | 38, 41 | mpbir 230 |
. . . . 5
β’
(+gβndx) β (Baseβndx) |
43 | | fvex 6860 |
. . . . . 6
β’
(.rβπ
) β V |
44 | | fvex 6860 |
. . . . . . 7
β’
(Baseβπ
)
β V |
45 | 44 | inex2 5280 |
. . . . . 6
β’ (π΄ β© (Baseβπ
)) β V |
46 | | fvex 6860 |
. . . . . . 7
β’
(+gβndx) β V |
47 | | fvex 6860 |
. . . . . . 7
β’
(Baseβndx) β V |
48 | 46, 47 | setscom 17059 |
. . . . . 6
β’ (((π
β π β§ (+gβndx) β
(Baseβndx)) β§ ((.rβπ
) β V β§ (π΄ β© (Baseβπ
)) β V)) β ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
49 | 43, 45, 48 | mpanr12 704 |
. . . . 5
β’ ((π
β π β§ (+gβndx) β
(Baseβndx)) β ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
50 | 28, 42, 49 | sylancl 587 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
51 | 36, 50 | eqtr4d 2780 |
. . 3
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (mulGrpβπ) = ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
52 | 19, 24, 51 | 3eqtr4a 2803 |
. 2
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (π βΎs π΄) = (mulGrpβπ)) |
53 | 16, 52 | pm2.61dan 812 |
1
β’ ((π
β π β§ π΄ β π) β (π βΎs π΄) = (mulGrpβπ)) |