Step |
Hyp |
Ref |
Expression |
1 |
|
ovres |
|- ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) ) |
2 |
1
|
adantl |
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) ) |
3 |
|
fndm |
|- ( G Fn ( C X. D ) -> dom G = ( C X. D ) ) |
4 |
3
|
reseq2d |
|- ( G Fn ( C X. D ) -> ( F |` dom G ) = ( F |` ( C X. D ) ) ) |
5 |
4
|
3ad2ant2 |
|- ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` dom G ) = ( F |` ( C X. D ) ) ) |
6 |
|
funssres |
|- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G ) |
7 |
6
|
3adant2 |
|- ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` dom G ) = G ) |
8 |
5 7
|
eqtr3d |
|- ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` ( C X. D ) ) = G ) |
9 |
8
|
oveqd |
|- ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( A ( F |` ( C X. D ) ) B ) = ( A G B ) ) |
10 |
9
|
adantr |
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A ( F |` ( C X. D ) ) B ) = ( A G B ) ) |
11 |
2 10
|
eqtr3d |
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A F B ) = ( A G B ) ) |