Step | Hyp | Ref
| Expression |
1 | | df-ov 7361 |
. . . . 5
β’ (π΄πΉπ΅) = (πΉββ¨π΄, π΅β©) |
2 | | xpsadd.3 |
. . . . . 6
β’ (π β π΄ β π) |
3 | | xpsadd.4 |
. . . . . 6
β’ (π β π΅ β π) |
4 | | xpsaddlem.f |
. . . . . . 7
β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
5 | 4 | xpsfval 17449 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄πΉπ΅) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
6 | 2, 3, 5 | syl2anc 585 |
. . . . 5
β’ (π β (π΄πΉπ΅) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
7 | 1, 6 | eqtr3id 2791 |
. . . 4
β’ (π β (πΉββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©}) |
8 | 2, 3 | opelxpd 5672 |
. . . . 5
β’ (π β β¨π΄, π΅β© β (π Γ π)) |
9 | 4 | xpsff1o2 17452 |
. . . . . . 7
β’ πΉ:(π Γ π)β1-1-ontoβran
πΉ |
10 | | f1of 6785 |
. . . . . . 7
β’ (πΉ:(π Γ π)β1-1-ontoβran
πΉ β πΉ:(π Γ π)βΆran πΉ) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
β’ πΉ:(π Γ π)βΆran πΉ |
12 | 11 | ffvelcdmi 7035 |
. . . . 5
β’
(β¨π΄, π΅β© β (π Γ π) β (πΉββ¨π΄, π΅β©) β ran πΉ) |
13 | 8, 12 | syl 17 |
. . . 4
β’ (π β (πΉββ¨π΄, π΅β©) β ran πΉ) |
14 | 7, 13 | eqeltrrd 2839 |
. . 3
β’ (π β {β¨β
, π΄β©, β¨1o,
π΅β©} β ran πΉ) |
15 | | df-ov 7361 |
. . . . 5
β’ (πΆπΉπ·) = (πΉββ¨πΆ, π·β©) |
16 | | xpsadd.5 |
. . . . . 6
β’ (π β πΆ β π) |
17 | | xpsadd.6 |
. . . . . 6
β’ (π β π· β π) |
18 | 4 | xpsfval 17449 |
. . . . . 6
β’ ((πΆ β π β§ π· β π) β (πΆπΉπ·) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . 5
β’ (π β (πΆπΉπ·) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
20 | 15, 19 | eqtr3id 2791 |
. . . 4
β’ (π β (πΉββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©}) |
21 | 16, 17 | opelxpd 5672 |
. . . . 5
β’ (π β β¨πΆ, π·β© β (π Γ π)) |
22 | 11 | ffvelcdmi 7035 |
. . . . 5
β’
(β¨πΆ, π·β© β (π Γ π) β (πΉββ¨πΆ, π·β©) β ran πΉ) |
23 | 21, 22 | syl 17 |
. . . 4
β’ (π β (πΉββ¨πΆ, π·β©) β ran πΉ) |
24 | 20, 23 | eqeltrrd 2839 |
. . 3
β’ (π β {β¨β
, πΆβ©, β¨1o,
π·β©} β ran πΉ) |
25 | | xpsaddlem.1 |
. . 3
β’ ((π β§ {β¨β
, π΄β©, β¨1o,
π΅β©} β ran πΉ β§ {β¨β
, πΆβ©, β¨1o,
π·β©} β ran πΉ) β ((β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©})) = (β‘πΉβ({β¨β
, π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©}))) |
26 | 14, 24, 25 | mpd3an23 1464 |
. 2
β’ (π β ((β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©})) = (β‘πΉβ({β¨β
, π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©}))) |
27 | | f1ocnvfv 7225 |
. . . . 5
β’ ((πΉ:(π Γ π)β1-1-ontoβran
πΉ β§ β¨π΄, π΅β© β (π Γ π)) β ((πΉββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©} β (β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) = β¨π΄, π΅β©)) |
28 | 9, 8, 27 | sylancr 588 |
. . . 4
β’ (π β ((πΉββ¨π΄, π΅β©) = {β¨β
, π΄β©, β¨1o, π΅β©} β (β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) = β¨π΄, π΅β©)) |
29 | 7, 28 | mpd 15 |
. . 3
β’ (π β (β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) = β¨π΄, π΅β©) |
30 | | f1ocnvfv 7225 |
. . . . 5
β’ ((πΉ:(π Γ π)β1-1-ontoβran
πΉ β§ β¨πΆ, π·β© β (π Γ π)) β ((πΉββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©} β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©}) = β¨πΆ, π·β©)) |
31 | 9, 21, 30 | sylancr 588 |
. . . 4
β’ (π β ((πΉββ¨πΆ, π·β©) = {β¨β
, πΆβ©, β¨1o, π·β©} β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©}) = β¨πΆ, π·β©)) |
32 | 20, 31 | mpd 15 |
. . 3
β’ (π β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©}) = β¨πΆ, π·β©) |
33 | 29, 32 | oveq12d 7376 |
. 2
β’ (π β ((β‘πΉβ{β¨β
, π΄β©, β¨1o, π΅β©}) β (β‘πΉβ{β¨β
, πΆβ©, β¨1o, π·β©})) = (β¨π΄, π΅β© β β¨πΆ, π·β©)) |
34 | | iftrue 4493 |
. . . . . . . . . . . 12
β’ (π = β
β if(π = β
, π
, π) = π
) |
35 | 34 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π = β
β (πΈβif(π = β
, π
, π)) = (πΈβπ
)) |
36 | | xpsaddlem.m |
. . . . . . . . . . 11
β’ Β· =
(πΈβπ
) |
37 | 35, 36 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = β
β (πΈβif(π = β
, π
, π)) = Β· ) |
38 | | iftrue 4493 |
. . . . . . . . . 10
β’ (π = β
β if(π = β
, π΄, π΅) = π΄) |
39 | | iftrue 4493 |
. . . . . . . . . 10
β’ (π = β
β if(π = β
, πΆ, π·) = πΆ) |
40 | 37, 38, 39 | oveq123d 7379 |
. . . . . . . . 9
β’ (π = β
β (if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·)) = (π΄ Β· πΆ)) |
41 | | iftrue 4493 |
. . . . . . . . 9
β’ (π = β
β if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·)) = (π΄ Β· πΆ)) |
42 | 40, 41 | eqtr4d 2780 |
. . . . . . . 8
β’ (π = β
β (if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·)) = if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·))) |
43 | | iffalse 4496 |
. . . . . . . . . . . 12
β’ (Β¬
π = β
β if(π = β
, π
, π) = π) |
44 | 43 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (Β¬
π = β
β (πΈβif(π = β
, π
, π)) = (πΈβπ)) |
45 | | xpsaddlem.n |
. . . . . . . . . . 11
β’ Γ =
(πΈβπ) |
46 | 44, 45 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (Β¬
π = β
β (πΈβif(π = β
, π
, π)) = Γ ) |
47 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π = β
β if(π = β
, π΄, π΅) = π΅) |
48 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π = β
β if(π = β
, πΆ, π·) = π·) |
49 | 46, 47, 48 | oveq123d 7379 |
. . . . . . . . 9
β’ (Β¬
π = β
β
(if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·)) = (π΅ Γ π·)) |
50 | | iffalse 4496 |
. . . . . . . . 9
β’ (Β¬
π = β
β if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·)) = (π΅ Γ π·)) |
51 | 49, 50 | eqtr4d 2780 |
. . . . . . . 8
β’ (Β¬
π = β
β
(if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·)) = if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·))) |
52 | 42, 51 | pm2.61i 182 |
. . . . . . 7
β’ (if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·)) = if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·)) |
53 | | xpsval.1 |
. . . . . . . . . . 11
β’ (π β π
β π) |
54 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β 2o) β π
β π) |
55 | | xpsval.2 |
. . . . . . . . . . 11
β’ (π β π β π) |
56 | 55 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β 2o) β π β π) |
57 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β 2o) β π β
2o) |
58 | | fvprif 17444 |
. . . . . . . . . 10
β’ ((π
β π β§ π β π β§ π β 2o) β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = if(π = β
, π
, π)) |
59 | 54, 56, 57, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β 2o) β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = if(π = β
, π
, π)) |
60 | 59 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π β 2o) β (πΈβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)) = (πΈβif(π = β
, π
, π))) |
61 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β 2o) β π΄ β π) |
62 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β 2o) β π΅ β π) |
63 | | fvprif 17444 |
. . . . . . . . 9
β’ ((π΄ β π β§ π΅ β π β§ π β 2o) β
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ) = if(π = β
, π΄, π΅)) |
64 | 61, 62, 57, 63 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β 2o) β
({β¨β
, π΄β©,
β¨1o, π΅β©}βπ) = if(π = β
, π΄, π΅)) |
65 | 16 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β 2o) β πΆ β π) |
66 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β 2o) β π· β π) |
67 | | fvprif 17444 |
. . . . . . . . 9
β’ ((πΆ β π β§ π· β π β§ π β 2o) β
({β¨β
, πΆβ©,
β¨1o, π·β©}βπ) = if(π = β
, πΆ, π·)) |
68 | 65, 66, 57, 67 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β 2o) β
({β¨β
, πΆβ©,
β¨1o, π·β©}βπ) = if(π = β
, πΆ, π·)) |
69 | 60, 64, 68 | oveq123d 7379 |
. . . . . . 7
β’ ((π β§ π β 2o) β
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(πΈβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ)) = (if(π = β
, π΄, π΅)(πΈβif(π = β
, π
, π))if(π = β
, πΆ, π·))) |
70 | | xpsadd.7 |
. . . . . . . . 9
β’ (π β (π΄ Β· πΆ) β π) |
71 | 70 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β 2o) β (π΄ Β· πΆ) β π) |
72 | | xpsadd.8 |
. . . . . . . . 9
β’ (π β (π΅ Γ π·) β π) |
73 | 72 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β 2o) β (π΅ Γ π·) β π) |
74 | | fvprif 17444 |
. . . . . . . 8
β’ (((π΄ Β· πΆ) β π β§ (π΅ Γ π·) β π β§ π β 2o) β
({β¨β
, (π΄ Β· πΆ)β©, β¨1o,
(π΅ Γ π·)β©}βπ) = if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·))) |
75 | 71, 73, 57, 74 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β 2o) β
({β¨β
, (π΄ Β· πΆ)β©, β¨1o,
(π΅ Γ π·)β©}βπ) = if(π = β
, (π΄ Β· πΆ), (π΅ Γ π·))) |
76 | 52, 69, 75 | 3eqtr4a 2803 |
. . . . . 6
β’ ((π β§ π β 2o) β
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(πΈβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ)) = ({β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}βπ)) |
77 | 76 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π β 2o β¦
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(πΈβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ))) = (π β 2o β¦
({β¨β
, (π΄ Β· πΆ)β©, β¨1o,
(π΅ Γ π·)β©}βπ))) |
78 | | fnpr2o 17440 |
. . . . . . 7
β’ ((π
β π β§ π β π) β {β¨β
, π
β©, β¨1o, πβ©} Fn
2o) |
79 | 53, 55, 78 | syl2anc 585 |
. . . . . 6
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} Fn
2o) |
80 | | xpsval.t |
. . . . . . . 8
β’ π = (π
Γs π) |
81 | | xpsval.x |
. . . . . . . 8
β’ π = (Baseβπ
) |
82 | | xpsval.y |
. . . . . . . 8
β’ π = (Baseβπ) |
83 | | eqid 2737 |
. . . . . . . 8
β’
(Scalarβπ
) =
(Scalarβπ
) |
84 | | xpsaddlem.u |
. . . . . . . 8
β’ π = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
85 | 80, 81, 82, 53, 55, 4, 83, 84 | xpsrnbas 17454 |
. . . . . . 7
β’ (π β ran πΉ = (Baseβπ)) |
86 | 14, 85 | eleqtrd 2840 |
. . . . . 6
β’ (π β {β¨β
, π΄β©, β¨1o,
π΅β©} β
(Baseβπ)) |
87 | 24, 85 | eleqtrd 2840 |
. . . . . 6
β’ (π β {β¨β
, πΆβ©, β¨1o,
π·β©} β
(Baseβπ)) |
88 | | xpsaddlem.2 |
. . . . . 6
β’
(({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β§
{β¨β
, π΄β©,
β¨1o, π΅β©} β (Baseβπ) β§ {β¨β
, πΆβ©, β¨1o, π·β©} β (Baseβπ)) β ({β¨β
, π΄β©, β¨1o,
π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©}) = (π β 2o β¦
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(πΈβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ)))) |
89 | 79, 86, 87, 88 | syl3anc 1372 |
. . . . 5
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©}) = (π β 2o β¦
(({β¨β
, π΄β©,
β¨1o, π΅β©}βπ)(πΈβ({β¨β
, π
β©, β¨1o, πβ©}βπ))({β¨β
, πΆβ©, β¨1o, π·β©}βπ)))) |
90 | | fnpr2o 17440 |
. . . . . . 7
β’ (((π΄ Β· πΆ) β π β§ (π΅ Γ π·) β π) β {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©} Fn 2o) |
91 | 70, 72, 90 | syl2anc 585 |
. . . . . 6
β’ (π β {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©} Fn 2o) |
92 | | dffn5 6902 |
. . . . . 6
β’
({β¨β
, (π΄
Β·
πΆ)β©,
β¨1o, (π΅
Γ
π·)β©} Fn 2o
β {β¨β
, (π΄
Β·
πΆ)β©,
β¨1o, (π΅
Γ
π·)β©} = (π β 2o β¦
({β¨β
, (π΄ Β· πΆ)β©, β¨1o,
(π΅ Γ π·)β©}βπ))) |
93 | 91, 92 | sylib 217 |
. . . . 5
β’ (π β {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©} = (π β 2o β¦
({β¨β
, (π΄ Β· πΆ)β©, β¨1o,
(π΅ Γ π·)β©}βπ))) |
94 | 77, 89, 93 | 3eqtr4d 2787 |
. . . 4
β’ (π β ({β¨β
, π΄β©, β¨1o,
π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©}) = {β¨β
,
(π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) |
95 | 94 | fveq2d 6847 |
. . 3
β’ (π β (β‘πΉβ({β¨β
, π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©})) = (β‘πΉβ{β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©})) |
96 | | df-ov 7361 |
. . . . 5
β’ ((π΄ Β· πΆ)πΉ(π΅ Γ π·)) = (πΉββ¨(π΄ Β· πΆ), (π΅ Γ π·)β©) |
97 | 4 | xpsfval 17449 |
. . . . . 6
β’ (((π΄ Β· πΆ) β π β§ (π΅ Γ π·) β π) β ((π΄ Β· πΆ)πΉ(π΅ Γ π·)) = {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) |
98 | 70, 72, 97 | syl2anc 585 |
. . . . 5
β’ (π β ((π΄ Β· πΆ)πΉ(π΅ Γ π·)) = {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) |
99 | 96, 98 | eqtr3id 2791 |
. . . 4
β’ (π β (πΉββ¨(π΄ Β· πΆ), (π΅ Γ π·)β©) = {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) |
100 | 70, 72 | opelxpd 5672 |
. . . . 5
β’ (π β β¨(π΄ Β· πΆ), (π΅ Γ π·)β© β (π Γ π)) |
101 | | f1ocnvfv 7225 |
. . . . 5
β’ ((πΉ:(π Γ π)β1-1-ontoβran
πΉ β§ β¨(π΄ Β· πΆ), (π΅ Γ π·)β© β (π Γ π)) β ((πΉββ¨(π΄ Β· πΆ), (π΅ Γ π·)β©) = {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©} β (β‘πΉβ{β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©)) |
102 | 9, 100, 101 | sylancr 588 |
. . . 4
β’ (π β ((πΉββ¨(π΄ Β· πΆ), (π΅ Γ π·)β©) = {β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©} β (β‘πΉβ{β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©)) |
103 | 99, 102 | mpd 15 |
. . 3
β’ (π β (β‘πΉβ{β¨β
, (π΄ Β· πΆ)β©, β¨1o, (π΅ Γ π·)β©}) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) |
104 | 95, 103 | eqtrd 2777 |
. 2
β’ (π β (β‘πΉβ({β¨β
, π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β
, πΆβ©, β¨1o, π·β©})) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) |
105 | 26, 33, 104 | 3eqtr3d 2785 |
1
β’ (π β (β¨π΄, π΅β© β β¨πΆ, π·β©) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) |