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 | | basendxnplusgndx 17170 |
. . . . . 6
β’
(Baseβndx) β (+gβndx) |
38 | 37 | necomi 2999 |
. . . . 5
β’
(+gβndx) β (Baseβndx) |
39 | | fvex 6860 |
. . . . . 6
β’
(.rβπ
) β V |
40 | | fvex 6860 |
. . . . . . 7
β’
(Baseβπ
)
β V |
41 | 40 | inex2 5280 |
. . . . . 6
β’ (π΄ β© (Baseβπ
)) β V |
42 | | fvex 6860 |
. . . . . . 7
β’
(+gβndx) β V |
43 | | fvex 6860 |
. . . . . . 7
β’
(Baseβndx) β V |
44 | 42, 43 | 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βπ
)β©)) |
45 | 39, 41, 44 | mpanr12 704 |
. . . . 5
β’ ((π
β π β§ (+gβndx) β
(Baseβndx)) β ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
46 | 28, 38, 45 | sylancl 587 |
. . . 4
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) = ((π
sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©) sSet
β¨(+gβndx), (.rβπ
)β©)) |
47 | 36, 46 | eqtr4d 2780 |
. . 3
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (mulGrpβπ) = ((π
sSet β¨(+gβndx),
(.rβπ
)β©) sSet β¨(Baseβndx), (π΄ β© (Baseβπ
))β©)) |
48 | 19, 24, 47 | 3eqtr4a 2803 |
. 2
β’ (((π
β π β§ π΄ β π) β§ Β¬ (Baseβπ
) β π΄) β (π βΎs π΄) = (mulGrpβπ)) |
49 | 16, 48 | pm2.61dan 812 |
1
β’ ((π
β π β§ π΄ β π) β (π βΎs π΄) = (mulGrpβπ)) |