Step | Hyp | Ref
| Expression |
1 | | xpsval.t |
. 2
β’ π = (π
Γs π) |
2 | | xpsval.1 |
. . . 4
β’ (π β π
β π) |
3 | 2 | elexd 3466 |
. . 3
β’ (π β π
β V) |
4 | | xpsval.2 |
. . . 4
β’ (π β π β π) |
5 | 4 | elexd 3466 |
. . 3
β’ (π β π β V) |
6 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
7 | | xpsval.x |
. . . . . . . . 9
β’ π = (Baseβπ
) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = π
β (Baseβπ) = π) |
9 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (Baseβπ ) = (Baseβπ)) |
10 | | xpsval.y |
. . . . . . . . 9
β’ π = (Baseβπ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = π β (Baseβπ ) = π) |
12 | | mpoeq12 7431 |
. . . . . . . 8
β’
(((Baseβπ) =
π β§ (Baseβπ ) = π) β (π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
13 | 8, 11, 12 | syl2an 597 |
. . . . . . 7
β’ ((π = π
β§ π = π) β (π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
14 | | xpsval.f |
. . . . . . 7
β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . 6
β’ ((π = π
β§ π = π) β (π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = πΉ) |
16 | 15 | cnveqd 5832 |
. . . . 5
β’ ((π = π
β§ π = π) β β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = β‘πΉ) |
17 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π
β (Scalarβπ) = (Scalarβπ
)) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((π = π
β§ π = π) β (Scalarβπ) = (Scalarβπ
)) |
19 | | xpsval.k |
. . . . . . . 8
β’ πΊ = (Scalarβπ
) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . 7
β’ ((π = π
β§ π = π) β (Scalarβπ) = πΊ) |
21 | | simpl 484 |
. . . . . . . . 9
β’ ((π = π
β§ π = π) β π = π
) |
22 | 21 | opeq2d 4838 |
. . . . . . . 8
β’ ((π = π
β§ π = π) β β¨β
, πβ© = β¨β
, π
β©) |
23 | | simpr 486 |
. . . . . . . . 9
β’ ((π = π
β§ π = π) β π = π) |
24 | 23 | opeq2d 4838 |
. . . . . . . 8
β’ ((π = π
β§ π = π) β β¨1o, π β© = β¨1o,
πβ©) |
25 | 22, 24 | preq12d 4703 |
. . . . . . 7
β’ ((π = π
β§ π = π) β {β¨β
, πβ©, β¨1o, π β©} = {β¨β
, π
β©, β¨1o,
πβ©}) |
26 | 20, 25 | oveq12d 7376 |
. . . . . 6
β’ ((π = π
β§ π = π) β ((Scalarβπ)Xs{β¨β
, πβ©, β¨1o, π β©}) = (πΊXs{β¨β
, π
β©, β¨1o, πβ©})) |
27 | | xpsval.u |
. . . . . 6
β’ π = (πΊXs{β¨β
, π
β©, β¨1o, πβ©}) |
28 | 26, 27 | eqtr4di 2795 |
. . . . 5
β’ ((π = π
β§ π = π) β ((Scalarβπ)Xs{β¨β
, πβ©, β¨1o, π β©}) = π) |
29 | 16, 28 | oveq12d 7376 |
. . . 4
β’ ((π = π
β§ π = π) β (β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ)Xs{β¨β
, πβ©, β¨1o, π β©})) = (β‘πΉ βs π)) |
30 | | df-xps 17393 |
. . . 4
β’
Γs = (π β V, π β V β¦ (β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ)Xs{β¨β
, πβ©, β¨1o, π β©}))) |
31 | | ovex 7391 |
. . . 4
β’ (β‘πΉ βs π) β V |
32 | 29, 30, 31 | ovmpoa 7511 |
. . 3
β’ ((π
β V β§ π β V) β (π
Γs
π) = (β‘πΉ βs π)) |
33 | 3, 5, 32 | syl2anc 585 |
. 2
β’ (π β (π
Γs π) = (β‘πΉ βs π)) |
34 | 1, 33 | eqtrid 2789 |
1
β’ (π β π = (β‘πΉ βs π)) |