Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
((Scalarβπ
)Xs(πΌ Γ {π
})) = ((Scalarβπ
)Xs(πΌ Γ {π
})) |
2 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
}))) = (mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
3 | | eqid 2733 |
. . . . . 6
β’
((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))) = ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))) |
4 | | simpr 486 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β πΌ β π) |
5 | | fvexd 6861 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β (Scalarβπ
) β V) |
6 | | fnconstg 6734 |
. . . . . . 7
β’ (π
β π β (πΌ Γ {π
}) Fn πΌ) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β (πΌ Γ {π
}) Fn πΌ) |
8 | 1, 2, 3, 4, 5, 7 | prdsmgp 20042 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β
((Baseβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) = (Baseβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
})))) β§
(+gβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) =
(+gβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
})))))) |
9 | 8 | simpld 496 |
. . . 4
β’ ((π
β π β§ πΌ β π) β
(Baseβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) = (Baseβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))))) |
10 | | pwsmgp.n |
. . . . . 6
β’ π = (mulGrpβπ) |
11 | | pwsmgp.y |
. . . . . . . 8
β’ π = (π
βs πΌ) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβπ
) =
(Scalarβπ
) |
13 | 11, 12 | pwsval 17376 |
. . . . . . 7
β’ ((π
β π β§ πΌ β π) β π = ((Scalarβπ
)Xs(πΌ Γ {π
}))) |
14 | 13 | fveq2d 6850 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β (mulGrpβπ) = (mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
15 | 10, 14 | eqtrid 2785 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β π = (mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) |
16 | 15 | fveq2d 6850 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (Baseβπ) =
(Baseβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
}))))) |
17 | | pwsmgp.z |
. . . . . 6
β’ π = (π βs πΌ) |
18 | | pwsmgp.m |
. . . . . . . . 9
β’ π = (mulGrpβπ
) |
19 | 18 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
20 | | eqid 2733 |
. . . . . . . . 9
β’ (π βs πΌ) = (π βs πΌ) |
21 | | eqid 2733 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
22 | 20, 21 | pwsval 17376 |
. . . . . . . 8
β’ ((π β V β§ πΌ β π) β (π βs πΌ) = ((Scalarβπ)Xs(πΌ Γ {π}))) |
23 | 19, 4, 22 | sylancr 588 |
. . . . . . 7
β’ ((π
β π β§ πΌ β π) β (π βs πΌ) = ((Scalarβπ)Xs(πΌ Γ {π}))) |
24 | 18, 12 | mgpsca 19912 |
. . . . . . . . . 10
β’
(Scalarβπ
) =
(Scalarβπ) |
25 | 24 | eqcomi 2742 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ
) |
26 | 25 | a1i 11 |
. . . . . . . 8
β’ ((π
β π β§ πΌ β π) β (Scalarβπ) = (Scalarβπ
)) |
27 | 18 | sneqi 4601 |
. . . . . . . . . 10
β’ {π} = {(mulGrpβπ
)} |
28 | 27 | xpeq2i 5664 |
. . . . . . . . 9
β’ (πΌ Γ {π}) = (πΌ Γ {(mulGrpβπ
)}) |
29 | | fnmgp 19906 |
. . . . . . . . . 10
β’ mulGrp Fn
V |
30 | | elex 3465 |
. . . . . . . . . . 11
β’ (π
β π β π
β V) |
31 | 30 | adantr 482 |
. . . . . . . . . 10
β’ ((π
β π β§ πΌ β π) β π
β V) |
32 | | fcoconst 7084 |
. . . . . . . . . 10
β’ ((mulGrp
Fn V β§ π
β V)
β (mulGrp β (πΌ
Γ {π
})) = (πΌ Γ {(mulGrpβπ
)})) |
33 | 29, 31, 32 | sylancr 588 |
. . . . . . . . 9
β’ ((π
β π β§ πΌ β π) β (mulGrp β (πΌ Γ {π
})) = (πΌ Γ {(mulGrpβπ
)})) |
34 | 28, 33 | eqtr4id 2792 |
. . . . . . . 8
β’ ((π
β π β§ πΌ β π) β (πΌ Γ {π}) = (mulGrp β (πΌ Γ {π
}))) |
35 | 26, 34 | oveq12d 7379 |
. . . . . . 7
β’ ((π
β π β§ πΌ β π) β ((Scalarβπ)Xs(πΌ Γ {π})) = ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
})))) |
36 | 23, 35 | eqtrd 2773 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β (π βs πΌ) = ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
})))) |
37 | 17, 36 | eqtrid 2785 |
. . . . 5
β’ ((π
β π β§ πΌ β π) β π = ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
})))) |
38 | 37 | fveq2d 6850 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (Baseβπ) = (Baseβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))))) |
39 | 9, 16, 38 | 3eqtr4d 2783 |
. . 3
β’ ((π
β π β§ πΌ β π) β (Baseβπ) = (Baseβπ)) |
40 | | pwsmgp.b |
. . 3
β’ π΅ = (Baseβπ) |
41 | | pwsmgp.c |
. . 3
β’ πΆ = (Baseβπ) |
42 | 39, 40, 41 | 3eqtr4g 2798 |
. 2
β’ ((π
β π β§ πΌ β π) β π΅ = πΆ) |
43 | 8 | simprd 497 |
. . . 4
β’ ((π
β π β§ πΌ β π) β
(+gβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
})))) =
(+gβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))))) |
44 | 15 | fveq2d 6850 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (+gβπ) =
(+gβ(mulGrpβ((Scalarβπ
)Xs(πΌ Γ {π
}))))) |
45 | 37 | fveq2d 6850 |
. . . 4
β’ ((π
β π β§ πΌ β π) β (+gβπ) =
(+gβ((Scalarβπ
)Xs(mulGrp β (πΌ Γ {π
}))))) |
46 | 43, 44, 45 | 3eqtr4d 2783 |
. . 3
β’ ((π
β π β§ πΌ β π) β (+gβπ) = (+gβπ)) |
47 | | pwsmgp.p |
. . 3
β’ + =
(+gβπ) |
48 | | pwsmgp.q |
. . 3
β’ β =
(+gβπ) |
49 | 46, 47, 48 | 3eqtr4g 2798 |
. 2
β’ ((π
β π β§ πΌ β π) β + = β ) |
50 | 42, 49 | jca 513 |
1
β’ ((π
β π β§ πΌ β π) β (π΅ = πΆ β§ + = β )) |