Step |
Hyp |
Ref |
Expression |
1 |
|
df-sate |
|- SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) ) |
2 |
1
|
a1i |
|- ( ( M e. V /\ U e. W ) -> SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) ) ) |
3 |
|
id |
|- ( m = M -> m = M ) |
4 |
3
|
sqxpeqd |
|- ( m = M -> ( m X. m ) = ( M X. M ) ) |
5 |
4
|
ineq2d |
|- ( m = M -> ( _E i^i ( m X. m ) ) = ( _E i^i ( M X. M ) ) ) |
6 |
3 5
|
oveq12d |
|- ( m = M -> ( m Sat ( _E i^i ( m X. m ) ) ) = ( M Sat ( _E i^i ( M X. M ) ) ) ) |
7 |
6
|
fveq1d |
|- ( m = M -> ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) = ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ) |
8 |
7
|
adantr |
|- ( ( m = M /\ u = U ) -> ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) = ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ) |
9 |
|
simpr |
|- ( ( m = M /\ u = U ) -> u = U ) |
10 |
8 9
|
fveq12d |
|- ( ( m = M /\ u = U ) -> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) |
11 |
10
|
adantl |
|- ( ( ( M e. V /\ U e. W ) /\ ( m = M /\ u = U ) ) -> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) |
12 |
|
elex |
|- ( M e. V -> M e. _V ) |
13 |
12
|
adantr |
|- ( ( M e. V /\ U e. W ) -> M e. _V ) |
14 |
|
elex |
|- ( U e. W -> U e. _V ) |
15 |
14
|
adantl |
|- ( ( M e. V /\ U e. W ) -> U e. _V ) |
16 |
|
fvexd |
|- ( ( M e. V /\ U e. W ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) e. _V ) |
17 |
2 11 13 15 16
|
ovmpod |
|- ( ( M e. V /\ U e. W ) -> ( M SatE U ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) |