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