Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’ (πΊXs{β¨β
, π
β©, β¨1o, πβ©}) = (πΊXs{β¨β
, π
β©, β¨1o, πβ©}) |
2 | | xpssca.g |
. . . . 5
β’ πΊ = (Scalarβπ
) |
3 | 2 | fvexi 6857 |
. . . 4
β’ πΊ β V |
4 | 3 | a1i 11 |
. . 3
β’ (π β πΊ β V) |
5 | | prex 5390 |
. . . 4
β’
{β¨β
, π
β©, β¨1o, πβ©} β
V |
6 | 5 | a1i 11 |
. . 3
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} β
V) |
7 | 1, 4, 6 | prdssca 17339 |
. 2
β’ (π β πΊ = (Scalarβ(πΊXs{β¨β
, π
β©, β¨1o, πβ©}))) |
8 | | xpssca.t |
. . . 4
β’ π = (π
Γs π) |
9 | | eqid 2737 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
10 | | eqid 2737 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
11 | | xpssca.1 |
. . . 4
β’ (π β π
β π) |
12 | | xpssca.2 |
. . . 4
β’ (π β π β π) |
13 | | eqid 2737 |
. . . 4
β’ (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
14 | 8, 9, 10, 11, 12, 13, 2, 1 | xpsval 17453 |
. . 3
β’ (π β π = (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs (πΊXs{β¨β
, π
β©, β¨1o, πβ©}))) |
15 | 8, 9, 10, 11, 12, 13, 2, 1 | xpsrnbas 17454 |
. . 3
β’ (π β ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (Baseβ(πΊXs{β¨β
, π
β©, β¨1o, πβ©}))) |
16 | 13 | xpsff1o2 17452 |
. . . . 5
β’ (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβran
(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
17 | | f1ocnv 6797 |
. . . . 5
β’ ((π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):((Baseβπ
) Γ (Baseβπ))β1-1-ontoβran
(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ((Baseβπ
) Γ (Baseβπ))) |
18 | 16, 17 | mp1i 13 |
. . . 4
β’ (π β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ((Baseβπ
) Γ (Baseβπ))) |
19 | | f1ofo 6792 |
. . . 4
β’ (β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ((Baseβπ
) Γ (Baseβπ)) β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βontoβ((Baseβπ
) Γ (Baseβπ))) |
20 | 18, 19 | syl 17 |
. . 3
β’ (π β β‘(π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β (Baseβπ
), π¦ β (Baseβπ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βontoβ((Baseβπ
) Γ (Baseβπ))) |
21 | | ovexd 7393 |
. . 3
β’ (π β (πΊXs{β¨β
, π
β©, β¨1o, πβ©}) β
V) |
22 | | eqid 2737 |
. . 3
β’
(Scalarβ(πΊXs{β¨β
, π
β©, β¨1o, πβ©})) = (Scalarβ(πΊXs{β¨β
, π
β©, β¨1o, πβ©})) |
23 | 14, 15, 20, 21, 22 | imassca 17402 |
. 2
β’ (π β (Scalarβ(πΊXs{β¨β
, π
β©, β¨1o, πβ©})) = (Scalarβπ)) |
24 | 7, 23 | eqtrd 2777 |
1
β’ (π β πΊ = (Scalarβπ)) |