Step | Hyp | Ref
| Expression |
1 | | xpsgrp.t |
. . 3
β’ π = (π
Γs π) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
4 | | simpl 484 |
. . 3
β’ ((π
β Grp β§ π β Grp) β π
β Grp) |
5 | | simpr 486 |
. . 3
β’ ((π
β Grp β§ π β Grp) β π β Grp) |
6 | | eqid 2733 |
. . 3
β’ (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
7 | | eqid 2733 |
. . 3
β’
(Scalarβπ
) =
(Scalarβπ
) |
8 | | eqid 2733 |
. . 3
β’
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17457 |
. 2
β’ ((π
β Grp β§ π β Grp) β π = (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
10 | 6 | xpsff1o2 17456 |
. . . . 5
β’ (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβran
(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17458 |
. . . . . 6
β’ ((π
β Grp β§ π β Grp) β ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
12 | 11 | f1oeq3d 6782 |
. . . . 5
β’ ((π
β Grp β§ π β Grp) β ((π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβran
(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβ(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})))) |
13 | 10, 12 | mpbii 232 |
. . . 4
β’ ((π
β Grp β§ π β Grp) β (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβ(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
14 | | f1ocnv 6797 |
. . . 4
β’ ((π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβ(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))β1-1-ontoβ((Baseβπ
) Γ (Baseβπ))) |
15 | | f1of1 6784 |
. . . 4
β’ (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))β1-1-ontoβ((Baseβπ
) Γ (Baseβπ)) β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))β1-1β((Baseβπ
) Γ (Baseβπ))) |
16 | 13, 14, 15 | 3syl 18 |
. . 3
β’ ((π
β Grp β§ π β Grp) β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))β1-1β((Baseβπ
) Γ (Baseβπ))) |
17 | | 2on 8427 |
. . . . 5
β’
2o β On |
18 | 17 | a1i 11 |
. . . 4
β’ ((π
β Grp β§ π β Grp) β
2o β On) |
19 | | fvexd 6858 |
. . . 4
β’ ((π
β Grp β§ π β Grp) β
(Scalarβπ
) β
V) |
20 | | xpscf 17452 |
. . . . 5
β’
({β¨β
, π
β©, β¨1o, πβ©}:2oβΆGrp
β (π
β Grp β§
π β
Grp)) |
21 | 20 | biimpri 227 |
. . . 4
β’ ((π
β Grp β§ π β Grp) β
{β¨β
, π
β©,
β¨1o, πβ©}:2oβΆGrp) |
22 | 8, 18, 19, 21 | prdsgrpd 18862 |
. . 3
β’ ((π
β Grp β§ π β Grp) β
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o,
πβ©}) β
Grp) |
23 | | eqid 2733 |
. . . 4
β’ (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) = (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) |
24 | | eqid 2733 |
. . . 4
β’
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) |
25 | 23, 24 | imasgrpf1 18869 |
. . 3
β’ ((β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))β1-1β((Baseβπ
) Γ (Baseβπ)) β§ ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) β Grp) β
(β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β
Grp) |
26 | 16, 22, 25 | syl2anc 585 |
. 2
β’ ((π
β Grp β§ π β Grp) β (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β
Grp) |
27 | 9, 26 | eqeltrd 2834 |
1
β’ ((π
β Grp β§ π β Grp) β π β Grp) |