Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
|
2 | | oveq12 6659 |
. . . . . . 7
LMHom LMHom |
3 | 2 | anidms 677 |
. . . . . 6
LMHom LMHom |
4 | | mendval.b |
. . . . . 6
LMHom |
5 | 3, 4 | syl6eqr 2674 |
. . . . 5
LMHom |
6 | 5 | csbeq1d 3540 |
. . . 4
LMHom
Scalar Scalar Scalar
Scalar Scalar Scalar |
7 | | ovex 6678 |
. . . . . 6
LMHom |
8 | 5, 7 | syl6eqelr 2710 |
. . . . 5
|
9 | | simpr 477 |
. . . . . . . 8
|
10 | 9 | opeq2d 4409 |
. . . . . . 7
|
11 | | fveq2 6191 |
. . . . . . . . . . . 12
|
12 | | ofeq 6899 |
. . . . . . . . . . . 12
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
|
14 | 13 | oveqdr 6674 |
. . . . . . . . . 10
|
15 | 9, 9, 14 | mpt2eq123dv 6717 |
. . . . . . . . 9
|
16 | | mendval.p |
. . . . . . . . 9
|
17 | 15, 16 | syl6eqr 2674 |
. . . . . . . 8
|
18 | 17 | opeq2d 4409 |
. . . . . . 7
|
19 | | eqidd 2623 |
. . . . . . . . . 10
|
20 | 9, 9, 19 | mpt2eq123dv 6717 |
. . . . . . . . 9
|
21 | | mendval.t |
. . . . . . . . 9
|
22 | 20, 21 | syl6eqr 2674 |
. . . . . . . 8
|
23 | 22 | opeq2d 4409 |
. . . . . . 7
|
24 | 10, 18, 23 | tpeq123d 4283 |
. . . . . 6
|
25 | | fveq2 6191 |
. . . . . . . . . 10
Scalar Scalar |
26 | 25 | adantr 481 |
. . . . . . . . 9
Scalar Scalar |
27 | | mendval.s |
. . . . . . . . 9
Scalar |
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . 8
Scalar |
29 | 28 | opeq2d 4409 |
. . . . . . 7
Scalar Scalar Scalar
|
30 | 28 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
31 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
32 | 31 | adantr 481 |
. . . . . . . . . . . 12
|
33 | | ofeq 6899 |
. . . . . . . . . . . 12
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
|
35 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
|
37 | 36 | xpeq1d 5138 |
. . . . . . . . . . 11
|
38 | | eqidd 2623 |
. . . . . . . . . . 11
|
39 | 34, 37, 38 | oveq123d 6671 |
. . . . . . . . . 10
|
40 | 30, 9, 39 | mpt2eq123dv 6717 |
. . . . . . . . 9
Scalar |
41 | | mendval.v |
. . . . . . . . 9
|
42 | 40, 41 | syl6eqr 2674 |
. . . . . . . 8
Scalar |
43 | 42 | opeq2d 4409 |
. . . . . . 7
Scalar
|
44 | 29, 43 | preq12d 4276 |
. . . . . 6
Scalar
Scalar Scalar Scalar |
45 | 24, 44 | uneq12d 3768 |
. . . . 5
Scalar Scalar Scalar
Scalar |
46 | 8, 45 | csbied 3560 |
. . . 4
Scalar Scalar Scalar
Scalar |
47 | 6, 46 | eqtrd 2656 |
. . 3
LMHom
Scalar Scalar Scalar
Scalar |
48 | | df-mend 37746 |
. . 3
MEndo
LMHom
Scalar Scalar Scalar |
49 | | tpex 6957 |
. . . 4
|
50 | | prex 4909 |
. . . 4
Scalar |
51 | 49, 50 | unex 6956 |
. . 3
Scalar |
52 | 47, 48, 51 | fvmpt 6282 |
. 2
MEndo
Scalar |
53 | 1, 52 | syl 17 |
1
MEndo
Scalar |