Step | Hyp | Ref
| Expression |
1 | | scmatval.s |
. 2
ScMat |
2 | | df-scmat 20297 |
. . . 4
ScMat Mat
|
3 | 2 | a1i 11 |
. . 3
ScMat
Mat
|
4 | | ovexd 6680 |
. . . . 5
Mat |
5 | | fveq2 6191 |
. . . . . . 7
Mat
Mat |
6 | | fveq2 6191 |
. . . . . . . . . 10
Mat
Mat |
7 | | eqidd 2623 |
. . . . . . . . . 10
Mat
|
8 | | fveq2 6191 |
. . . . . . . . . 10
Mat
Mat |
9 | 6, 7, 8 | oveq123d 6671 |
. . . . . . . . 9
Mat
Mat Mat |
10 | 9 | eqeq2d 2632 |
. . . . . . . 8
Mat
Mat Mat |
11 | 10 | rexbidv 3052 |
. . . . . . 7
Mat
Mat Mat |
12 | 5, 11 | rabeqbidv 3195 |
. . . . . 6
Mat
Mat Mat
Mat
|
13 | 12 | adantl 482 |
. . . . 5
Mat
Mat Mat
Mat
|
14 | 4, 13 | csbied 3560 |
. . . 4
Mat
Mat Mat
Mat
|
15 | | oveq12 6659 |
. . . . . . . 8
Mat Mat |
16 | 15 | fveq2d 6195 |
. . . . . . 7
Mat Mat |
17 | | scmatval.b |
. . . . . . . 8
|
18 | | scmatval.a |
. . . . . . . . 9
Mat |
19 | 18 | fveq2i 6194 |
. . . . . . . 8
Mat |
20 | 17, 19 | eqtri 2644 |
. . . . . . 7
Mat |
21 | 16, 20 | syl6eqr 2674 |
. . . . . 6
Mat |
22 | | fveq2 6191 |
. . . . . . . . 9
|
23 | | scmatval.k |
. . . . . . . . 9
|
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . 8
|
25 | 24 | adantl 482 |
. . . . . . 7
|
26 | 15 | fveq2d 6195 |
. . . . . . . . . 10
Mat
Mat |
27 | | scmatval.t |
. . . . . . . . . . 11
|
28 | 18 | fveq2i 6194 |
. . . . . . . . . . 11
Mat |
29 | 27, 28 | eqtri 2644 |
. . . . . . . . . 10
Mat |
30 | 26, 29 | syl6eqr 2674 |
. . . . . . . . 9
Mat |
31 | | eqidd 2623 |
. . . . . . . . 9
|
32 | 15 | fveq2d 6195 |
. . . . . . . . . 10
Mat
Mat |
33 | | scmatval.1 |
. . . . . . . . . . 11
|
34 | 18 | fveq2i 6194 |
. . . . . . . . . . 11
Mat |
35 | 33, 34 | eqtri 2644 |
. . . . . . . . . 10
Mat |
36 | 32, 35 | syl6eqr 2674 |
. . . . . . . . 9
Mat |
37 | 30, 31, 36 | oveq123d 6671 |
. . . . . . . 8
Mat Mat |
38 | 37 | eqeq2d 2632 |
. . . . . . 7
Mat
Mat
|
39 | 25, 38 | rexeqbidv 3153 |
. . . . . 6
Mat
Mat
|
40 | 21, 39 | rabeqbidv 3195 |
. . . . 5
Mat Mat Mat
|
41 | 40 | adantl 482 |
. . . 4
Mat
Mat Mat
|
42 | 14, 41 | eqtrd 2656 |
. . 3
Mat
|
43 | | simpl 473 |
. . 3
|
44 | | elex 3212 |
. . . 4
|
45 | 44 | adantl 482 |
. . 3
|
46 | | fvex 6201 |
. . . . . 6
|
47 | 17, 46 | eqeltri 2697 |
. . . . 5
|
48 | 47 | rabex 4813 |
. . . 4
|
49 | 48 | a1i 11 |
. . 3
|
50 | 3, 42, 43, 45, 49 | ovmpt2d 6788 |
. 2
ScMat
|
51 | 1, 50 | syl5eq 2668 |
1
|