Step | Hyp | Ref
| Expression |
1 | | xpsvsca.3 |
. . 3
|
2 | | df-ov 6653 |
. . . . 5
|
3 | | xpsvsca.4 |
. . . . . 6
|
4 | | xpsvsca.5 |
. . . . . 6
|
5 | | eqid 2622 |
. . . . . . 7
|
6 | 5 | xpsfval 16227 |
. . . . . 6
|
7 | 3, 4, 6 | syl2anc 693 |
. . . . 5
|
8 | 2, 7 | syl5eqr 2670 |
. . . 4
|
9 | | opelxpi 5148 |
. . . . . 6
|
10 | 3, 4, 9 | syl2anc 693 |
. . . . 5
|
11 | 5 | xpsff1o2 16231 |
. . . . . . 7
|
12 | | f1of 6137 |
. . . . . . 7
|
13 | 11, 12 | ax-mp 5 |
. . . . . 6
|
14 | 13 | ffvelrni 6358 |
. . . . 5
|
15 | 10, 14 | syl 17 |
. . . 4
|
16 | 8, 15 | eqeltrrd 2702 |
. . 3
|
17 | | xpssca.t |
. . . . 5
s |
18 | | xpsvsca.x |
. . . . 5
|
19 | | xpsvsca.y |
. . . . 5
|
20 | | xpssca.1 |
. . . . 5
|
21 | | xpssca.2 |
. . . . 5
|
22 | | xpssca.g |
. . . . 5
Scalar |
23 | | eqid 2622 |
. . . . 5
s s |
24 | 17, 18, 19, 20, 21, 5, 22, 23 | xpsval 16232 |
. . . 4
s
s |
25 | 17, 18, 19, 20, 21, 5, 22, 23 | xpslem 16233 |
. . . 4
s |
26 | | f1ocnv 6149 |
. . . . . 6
|
27 | 11, 26 | mp1i 13 |
. . . . 5
|
28 | | f1ofo 6144 |
. . . . 5
|
29 | 27, 28 | syl 17 |
. . . 4
|
30 | | ovexd 6680 |
. . . 4
s |
31 | | fvex 6201 |
. . . . . . . 8
Scalar |
32 | 22, 31 | eqeltri 2697 |
. . . . . . 7
|
33 | 32 | a1i 11 |
. . . . . 6
|
34 | | ovex 6678 |
. . . . . . . 8
|
35 | 34 | cnvex 7113 |
. . . . . . 7
|
36 | 35 | a1i 11 |
. . . . . 6
|
37 | 23, 33, 36 | prdssca 16116 |
. . . . 5
Scalars |
38 | 37 | trud 1493 |
. . . 4
Scalars |
39 | | xpsvsca.k |
. . . 4
|
40 | | eqid 2622 |
. . . 4
s s |
41 | | xpsvsca.p |
. . . 4
|
42 | 27 | f1ovscpbl 16186 |
. . . 4
s s |
43 | 24, 25, 29, 30, 38, 39, 40, 41, 42 | imasvscaval 16198 |
. . 3
s |
44 | 1, 16, 43 | mpd3an23 1426 |
. 2
s |
45 | | f1ocnvfv 6534 |
. . . . 5
|
46 | 11, 10, 45 | sylancr 695 |
. . . 4
|
47 | 8, 46 | mpd 15 |
. . 3
|
48 | 47 | oveq2d 6666 |
. 2
|
49 | | iftrue 4092 |
. . . . . . . . . . . 12
|
50 | 49 | fveq2d 6195 |
. . . . . . . . . . 11
|
51 | | xpsvsca.m |
. . . . . . . . . . 11
|
52 | 50, 51 | syl6eqr 2674 |
. . . . . . . . . 10
|
53 | | eqidd 2623 |
. . . . . . . . . 10
|
54 | | iftrue 4092 |
. . . . . . . . . 10
|
55 | 52, 53, 54 | oveq123d 6671 |
. . . . . . . . 9
|
56 | | iftrue 4092 |
. . . . . . . . 9
|
57 | 55, 56 | eqtr4d 2659 |
. . . . . . . 8
|
58 | | iffalse 4095 |
. . . . . . . . . . . 12
|
59 | 58 | fveq2d 6195 |
. . . . . . . . . . 11
|
60 | | xpsvsca.n |
. . . . . . . . . . 11
|
61 | 59, 60 | syl6eqr 2674 |
. . . . . . . . . 10
|
62 | | eqidd 2623 |
. . . . . . . . . 10
|
63 | | iffalse 4095 |
. . . . . . . . . 10
|
64 | 61, 62, 63 | oveq123d 6671 |
. . . . . . . . 9
|
65 | | iffalse 4095 |
. . . . . . . . 9
|
66 | 64, 65 | eqtr4d 2659 |
. . . . . . . 8
|
67 | 57, 66 | pm2.61i 176 |
. . . . . . 7
|
68 | 20 | adantr 481 |
. . . . . . . . . 10
|
69 | 21 | adantr 481 |
. . . . . . . . . 10
|
70 | | simpr 477 |
. . . . . . . . . 10
|
71 | | xpscfv 16222 |
. . . . . . . . . 10
|
72 | 68, 69, 70, 71 | syl3anc 1326 |
. . . . . . . . 9
|
73 | 72 | fveq2d 6195 |
. . . . . . . 8
|
74 | | eqidd 2623 |
. . . . . . . 8
|
75 | 3 | adantr 481 |
. . . . . . . . 9
|
76 | 4 | adantr 481 |
. . . . . . . . 9
|
77 | | xpscfv 16222 |
. . . . . . . . 9
|
78 | 75, 76, 70, 77 | syl3anc 1326 |
. . . . . . . 8
|
79 | 73, 74, 78 | oveq123d 6671 |
. . . . . . 7
|
80 | | xpsvsca.6 |
. . . . . . . . 9
|
81 | 80 | adantr 481 |
. . . . . . . 8
|
82 | | xpsvsca.7 |
. . . . . . . . 9
|
83 | 82 | adantr 481 |
. . . . . . . 8
|
84 | | xpscfv 16222 |
. . . . . . . 8
|
85 | 81, 83, 70, 84 | syl3anc 1326 |
. . . . . . 7
|
86 | 67, 79, 85 | 3eqtr4a 2682 |
. . . . . 6
|
87 | 86 | mpteq2dva 4744 |
. . . . 5
|
88 | | eqid 2622 |
. . . . . 6
s s |
89 | 32 | a1i 11 |
. . . . . 6
|
90 | | 2on 7568 |
. . . . . . 7
|
91 | 90 | a1i 11 |
. . . . . 6
|
92 | | xpscfn 16219 |
. . . . . . 7
|
93 | 20, 21, 92 | syl2anc 693 |
. . . . . 6
|
94 | 16, 25 | eleqtrd 2703 |
. . . . . 6
s |
95 | 23, 88, 40, 39, 89, 91, 93, 1, 94 | prdsvscaval 16139 |
. . . . 5
s |
96 | | xpscfn 16219 |
. . . . . . 7
|
97 | 80, 82, 96 | syl2anc 693 |
. . . . . 6
|
98 | | dffn5 6241 |
. . . . . 6
|
99 | 97, 98 | sylib 208 |
. . . . 5
|
100 | 87, 95, 99 | 3eqtr4d 2666 |
. . . 4
s
|
101 | 100 | fveq2d 6195 |
. . 3
s |
102 | | df-ov 6653 |
. . . . 5
|
103 | 5 | xpsfval 16227 |
. . . . . 6
|
104 | 80, 82, 103 | syl2anc 693 |
. . . . 5
|
105 | 102, 104 | syl5eqr 2670 |
. . . 4
|
106 | | opelxpi 5148 |
. . . . . 6
|
107 | 80, 82, 106 | syl2anc 693 |
. . . . 5
|
108 | | f1ocnvfv 6534 |
. . . . 5
|
109 | 11, 107, 108 | sylancr 695 |
. . . 4
|
110 | 105, 109 | mpd 15 |
. . 3
|
111 | 101, 110 | eqtrd 2656 |
. 2
s |
112 | 44, 48, 111 | 3eqtr3d 2664 |
1
|