Step | Hyp | Ref
| Expression |
1 | | df-ov 7361 |
. . . . 5
β’ (π΄(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π΅) = ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) |
2 | | xpsle.3 |
. . . . . 6
β’ (π β π΄ β π) |
3 | | xpsle.4 |
. . . . . 6
β’ (π β π΅ β π) |
4 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
5 | 4 | xpsfval 17449 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π΅) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
6 | 2, 3, 5 | syl2anc 585 |
. . . . 5
β’ (π β (π΄(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π΅) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
7 | 1, 6 | eqtr3id 2791 |
. . . 4
β’ (π β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
8 | 2, 3 | opelxpd 5672 |
. . . . 5
β’ (π β β¨π΄, π΅β© β (π Γ π)) |
9 | 4 | xpsff1o2 17452 |
. . . . . . 7
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
10 | | f1of 6785 |
. . . . . . 7
β’ ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)βΆran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)βΆran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
12 | 11 | ffvelcdmi 7035 |
. . . . 5
β’
(β¨π΄, π΅β© β (π Γ π) β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
13 | 8, 12 | syl 17 |
. . . 4
β’ (π β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
14 | 7, 13 | eqeltrrd 2839 |
. . 3
β’ (π β {β¨β
, π΄β©, β¨1o,
π΅β©} β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
15 | | df-ov 7361 |
. . . . 5
β’ (πΆ(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π·) = ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) |
16 | | xpsle.5 |
. . . . . 6
β’ (π β πΆ β π) |
17 | | xpsle.6 |
. . . . . 6
β’ (π β π· β π) |
18 | 4 | xpsfval 17449 |
. . . . . 6
β’ ((πΆ β π β§ π· β π) β (πΆ(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π·) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . 5
β’ (π β (πΆ(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})π·) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
20 | 15, 19 | eqtr3id 2791 |
. . . 4
β’ (π β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
21 | 16, 17 | opelxpd 5672 |
. . . . 5
β’ (π β β¨πΆ, π·β© β (π Γ π)) |
22 | 11 | ffvelcdmi 7035 |
. . . . 5
β’
(β¨πΆ, π·β© β (π Γ π) β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
23 | 21, 22 | syl 17 |
. . . 4
β’ (π β ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
24 | 20, 23 | eqeltrrd 2839 |
. . 3
β’ (π β {β¨β
, πΆβ©, β¨1o,
π·β©} β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
25 | | xpsle.t |
. . . . 5
β’ π = (π
Γs π) |
26 | | xpsle.x |
. . . . 5
β’ π = (Baseβπ
) |
27 | | xpsle.y |
. . . . 5
β’ π = (Baseβπ) |
28 | | xpsle.1 |
. . . . 5
β’ (π β π
β π) |
29 | | xpsle.2 |
. . . . 5
β’ (π β π β π) |
30 | | eqid 2737 |
. . . . 5
β’
(Scalarβπ
) =
(Scalarβπ
) |
31 | | eqid 2737 |
. . . . 5
β’
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
32 | 25, 26, 27, 28, 29, 4, 30, 31 | xpsval 17453 |
. . . 4
β’ (π β π = (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
33 | 25, 26, 27, 28, 29, 4, 30, 31 | xpsrnbas 17454 |
. . . 4
β’ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
34 | | f1ocnv 6797 |
. . . . . 6
β’ ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ(π Γ π)) |
35 | 9, 34 | mp1i 13 |
. . . . 5
β’ (π β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ(π Γ π)) |
36 | | f1ofo 6792 |
. . . . 5
β’ (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ(π Γ π) β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βontoβ(π Γ π)) |
37 | 35, 36 | syl 17 |
. . . 4
β’ (π β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βontoβ(π Γ π)) |
38 | | ovexd 7393 |
. . . 4
β’ (π β ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) β
V) |
39 | | xpsle.p |
. . . 4
β’ β€ =
(leβπ) |
40 | | eqid 2737 |
. . . 4
β’
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) |
41 | 35 | f1olecpbl 17410 |
. . . 4
β’ ((π β§ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β§ π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) β§ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β§ π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) β (((β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βπ) = (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βπ) β§ (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βπ) = (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})βπ)) β (π(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))π β π(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))π))) |
42 | 32, 33, 37, 38, 39, 40, 41 | imasleval 17424 |
. . 3
β’ ((π β§ {β¨β
, π΄β©, β¨1o,
π΅β©} β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β§ {β¨β
,
πΆβ©,
β¨1o, π·β©} β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) β ((β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) β€ (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) β {β¨β
, π΄β©, β¨1o,
π΅β©}
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})){β¨β
, πΆβ©, β¨1o,
π·β©})) |
43 | 14, 24, 42 | mpd3an23 1464 |
. 2
β’ (π β ((β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) β€ (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) β {β¨β
, π΄β©, β¨1o,
π΅β©}
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})){β¨β
, πΆβ©, β¨1o,
π·β©})) |
44 | | f1ocnvfv 7225 |
. . . . 5
β’ (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β§ β¨π΄, π΅β© β (π Γ π)) β (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©} β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) = β¨π΄, π΅β©)) |
45 | 9, 8, 44 | sylancr 588 |
. . . 4
β’ (π β (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©} β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) = β¨π΄, π΅β©)) |
46 | 7, 45 | mpd 15 |
. . 3
β’ (π β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) = β¨π΄, π΅β©) |
47 | | f1ocnvfv 7225 |
. . . . 5
β’ (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β§ β¨πΆ, π·β© β (π Γ π)) β (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©} β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) = β¨πΆ, π·β©)) |
48 | 9, 21, 47 | sylancr 588 |
. . . 4
β’ (π β (((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})ββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©} β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) = β¨πΆ, π·β©)) |
49 | 20, 48 | mpd 15 |
. . 3
β’ (π β (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) = β¨πΆ, π·β©) |
50 | 46, 49 | breq12d 5119 |
. 2
β’ (π β ((β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
π΄β©,
β¨1o, π΅β©}) β€ (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β{β¨β
,
πΆβ©,
β¨1o, π·β©}) β β¨π΄, π΅β© β€ β¨πΆ, π·β©)) |
51 | | eqid 2737 |
. . . 4
β’
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) |
52 | | fvexd 6858 |
. . . 4
β’ (π β (Scalarβπ
) β V) |
53 | | 2on 8427 |
. . . . 5
β’
2o β On |
54 | 53 | a1i 11 |
. . . 4
β’ (π β 2o β
On) |
55 | | fnpr2o 17440 |
. . . . 5
β’ ((π
β π β§ π β π) β {β¨β
, π
β©, β¨1o, πβ©} Fn
2o) |
56 | 28, 29, 55 | syl2anc 585 |
. . . 4
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} Fn
2o) |
57 | 14, 33 | eleqtrd 2840 |
. . . 4
β’ (π β {β¨β
, π΄β©, β¨1o,
π΅β©} β
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
58 | 24, 33 | eleqtrd 2840 |
. . . 4
β’ (π β {β¨β
, πΆβ©, β¨1o,
π·β©} β
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
59 | 31, 51, 52, 54, 56, 57, 58, 40 | prdsleval 17360 |
. . 3
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©}
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})){β¨β
, πΆβ©, β¨1o,
π·β©} β
βπ β
2o ({β¨β
, π΄β©, β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ))) |
60 | | df2o3 8421 |
. . . . . 6
β’
2o = {β
, 1o} |
61 | 60 | raleqi 3312 |
. . . . 5
β’
(βπ β
2o ({β¨β
, π΄β©, β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β βπ β {β
, 1o}
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ)) |
62 | | 0ex 5265 |
. . . . . 6
β’ β
β V |
63 | | 1oex 8423 |
. . . . . 6
β’
1o β V |
64 | | fveq2 6843 |
. . . . . . 7
β’ (π = β
β
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ) = ({β¨β
, π΄β©, β¨1o, π΅β©}ββ
)) |
65 | | 2fveq3 6848 |
. . . . . . 7
β’ (π = β
β
(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (leβ({β¨β
, π
β©, β¨1o,
πβ©}ββ
))) |
66 | | fveq2 6843 |
. . . . . . 7
β’ (π = β
β
({β¨β
, πΆβ©,
β¨1o, π·β©}βπ) = ({β¨β
, πΆβ©, β¨1o, π·β©}ββ
)) |
67 | 64, 65, 66 | breq123d 5120 |
. . . . . 6
β’ (π = β
β
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β ({β¨β
, π΄β©, β¨1o, π΅β©}ββ
)(leβ({β¨β
,
π
β©, β¨1o,
πβ©}ββ
))({β¨β
, πΆβ©, β¨1o, π·β©}ββ
))) |
68 | | fveq2 6843 |
. . . . . . 7
β’ (π = 1o β
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ) = ({β¨β
, π΄β©, β¨1o, π΅β©}β1o)) |
69 | | 2fveq3 6848 |
. . . . . . 7
β’ (π = 1o β
(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (leβ({β¨β
, π
β©, β¨1o,
πβ©}β1o))) |
70 | | fveq2 6843 |
. . . . . . 7
β’ (π = 1o β
({β¨β
, πΆβ©,
β¨1o, π·β©}βπ) = ({β¨β
, πΆβ©, β¨1o, π·β©}β1o)) |
71 | 68, 69, 70 | breq123d 5120 |
. . . . . 6
β’ (π = 1o β
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β ({β¨β
, π΄β©, β¨1o, π΅β©}β1o)(leβ({β¨β
,
π
β©, β¨1o, πβ©}β1o))({β¨β
, πΆβ©, β¨1o, π·β©}β1o))) |
72 | 62, 63, 67, 71 | ralpr 4662 |
. . . . 5
β’
(βπ β
{β
, 1o} ({β¨β
, π΄β©, β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β (({β¨β
, π΄β©, β¨1o, π΅β©}ββ
)(leβ({β¨β
,
π
β©, β¨1o,
πβ©}ββ
))({β¨β
, πΆβ©, β¨1o, π·β©}ββ
) β§
({β¨β
, π΄β©,
β¨1o, π΅β©}β1o)(leβ({β¨β
,
π
β©, β¨1o, πβ©}β1o))({β¨β
, πΆβ©, β¨1o, π·β©}β1o))) |
73 | 61, 72 | bitri 275 |
. . . 4
β’
(βπ β
2o ({β¨β
, π΄β©, β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β (({β¨β
, π΄β©, β¨1o, π΅β©}ββ
)(leβ({β¨β
,
π
β©, β¨1o,
πβ©}ββ
))({β¨β
, πΆβ©, β¨1o, π·β©}ββ
) β§
({β¨β
, π΄β©,
β¨1o, π΅β©}β1o)(leβ({β¨β
,
π
β©, β¨1o, πβ©}β1o))({β¨β
, πΆβ©, β¨1o, π·β©}β1o))) |
74 | | fvpr0o 17442 |
. . . . . . 7
β’ (π΄ β π β ({β¨β
, π΄β©, β¨1o, π΅β©}ββ
) = π΄) |
75 | 2, 74 | syl 17 |
. . . . . 6
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©}ββ
) =
π΄) |
76 | | fvpr0o 17442 |
. . . . . . . . 9
β’ (π
β π β ({β¨β
, π
β©, β¨1o, πβ©}ββ
) = π
) |
77 | 28, 76 | syl 17 |
. . . . . . . 8
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}ββ
) =
π
) |
78 | 77 | fveq2d 6847 |
. . . . . . 7
β’ (π β (leβ({β¨β
,
π
β©,
β¨1o, πβ©}ββ
)) = (leβπ
)) |
79 | | xpsle.m |
. . . . . . 7
β’ π = (leβπ
) |
80 | 78, 79 | eqtr4di 2795 |
. . . . . 6
β’ (π β (leβ({β¨β
,
π
β©,
β¨1o, πβ©}ββ
)) = π) |
81 | | fvpr0o 17442 |
. . . . . . 7
β’ (πΆ β π β ({β¨β
, πΆβ©, β¨1o, π·β©}ββ
) = πΆ) |
82 | 16, 81 | syl 17 |
. . . . . 6
β’ (π β ({β¨β
, πΆβ©, β¨1o,
π·β©}ββ
) =
πΆ) |
83 | 75, 80, 82 | breq123d 5120 |
. . . . 5
β’ (π β (({β¨β
, π΄β©, β¨1o,
π΅β©}ββ
)(leβ({β¨β
,
π
β©, β¨1o,
πβ©}ββ
))({β¨β
, πΆβ©, β¨1o, π·β©}ββ
) β π΄ππΆ)) |
84 | | fvpr1o 17443 |
. . . . . . 7
β’ (π΅ β π β ({β¨β
, π΄β©, β¨1o, π΅β©}β1o) =
π΅) |
85 | 3, 84 | syl 17 |
. . . . . 6
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©}β1o) = π΅) |
86 | | fvpr1o 17443 |
. . . . . . . . 9
β’ (π β π β ({β¨β
, π
β©, β¨1o, πβ©}β1o) =
π) |
87 | 29, 86 | syl 17 |
. . . . . . . 8
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}β1o) = π) |
88 | 87 | fveq2d 6847 |
. . . . . . 7
β’ (π β (leβ({β¨β
,
π
β©,
β¨1o, πβ©}β1o)) =
(leβπ)) |
89 | | xpsle.n |
. . . . . . 7
β’ π = (leβπ) |
90 | 88, 89 | eqtr4di 2795 |
. . . . . 6
β’ (π β (leβ({β¨β
,
π
β©,
β¨1o, πβ©}β1o)) = π) |
91 | | fvpr1o 17443 |
. . . . . . 7
β’ (π· β π β ({β¨β
, πΆβ©, β¨1o, π·β©}β1o) =
π·) |
92 | 17, 91 | syl 17 |
. . . . . 6
β’ (π β ({β¨β
, πΆβ©, β¨1o,
π·β©}β1o) = π·) |
93 | 85, 90, 92 | breq123d 5120 |
. . . . 5
β’ (π β (({β¨β
, π΄β©, β¨1o,
π΅β©}β1o)(leβ({β¨β
,
π
β©, β¨1o, πβ©}β1o))({β¨β
, πΆβ©, β¨1o, π·β©}β1o) β π΅ππ·)) |
94 | 83, 93 | anbi12d 632 |
. . . 4
β’ (π β ((({β¨β
, π΄β©, β¨1o,
π΅β©}ββ
)(leβ({β¨β
,
π
β©, β¨1o,
πβ©}ββ
))({β¨β
, πΆβ©, β¨1o, π·β©}ββ
) β§
({β¨β
, π΄β©,
β¨1o, π΅β©}β1o)(leβ({β¨β
,
π
β©, β¨1o, πβ©}β1o))({β¨β
, πΆβ©, β¨1o, π·β©}β1o)) β
(π΄ππΆ
β§ π΅ππ·))) |
95 | 73, 94 | bitrid 283 |
. . 3
β’ (π β (βπ β 2o
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(leβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ) β (π΄ππΆ β§ π΅ππ·))) |
96 | 59, 95 | bitrd 279 |
. 2
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©}
(leβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})){β¨β
, πΆβ©, β¨1o,
π·β©} β (π΄ππΆ β§ π΅ππ·))) |
97 | 43, 50, 96 | 3bitr3d 309 |
1
β’ (π β (β¨π΄, π΅β© β€ β¨πΆ, π·β© β (π΄ππΆ β§ π΅ππ·))) |