Description: A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mat2pmatfval.t | |
|
mat2pmatfval.a | |
||
mat2pmatfval.b | |
||
mat2pmatfval.p | |
||
mat2pmatfval.s | |
||
Assertion | mat2pmatvalel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mat2pmatfval.t | |
|
2 | mat2pmatfval.a | |
|
3 | mat2pmatfval.b | |
|
4 | mat2pmatfval.p | |
|
5 | mat2pmatfval.s | |
|
6 | 1 2 3 4 5 | mat2pmatval | |
7 | 6 | adantr | |
8 | oveq12 | |
|
9 | 8 | fveq2d | |
10 | 9 | adantl | |
11 | simprl | |
|
12 | simprr | |
|
13 | fvexd | |
|
14 | 7 10 11 12 13 | ovmpod | |