Metamath Proof Explorer

Theorem imasaddvallem

Description: The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f 
|- ( ph -> F : V -onto-> B )
imasaddf.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
imasaddflem.a 
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Assertion imasaddvallem 
|- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f 
 |-  ( ph -> F : V -onto-> B )
2 imasaddf.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
3 imasaddflem.a 
 |-  ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
4 df-ov 
 |-  ( ( F ` X ) .xb ( F ` Y ) ) = ( .xb ` <. ( F ` X ) , ( F ` Y ) >. )
5 1 2 3 imasaddfnlem 
 |-  ( ph -> .xb Fn ( B X. B ) )
6 fnfun 
 |-  ( .xb Fn ( B X. B ) -> Fun .xb )
7 5 6 syl 
 |-  ( ph -> Fun .xb )
8 7 3ad2ant1 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> Fun .xb )
9 fveq2 
 |-  ( p = X -> ( F ` p ) = ( F ` X ) )
10 9 opeq1d 
 |-  ( p = X -> <. ( F ` p ) , ( F ` Y ) >. = <. ( F ` X ) , ( F ` Y ) >. )
11 fvoveq1 
 |-  ( p = X -> ( F ` ( p .x. Y ) ) = ( F ` ( X .x. Y ) ) )
12 10 11 opeq12d 
 |-  ( p = X -> <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. = <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. )
13 12 sneqd 
 |-  ( p = X -> { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } = { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } )
14 13 ssiun2s 
 |-  ( X e. V -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } )
15 14 3ad2ant2 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } )
16 fveq2 
 |-  ( q = Y -> ( F ` q ) = ( F ` Y ) )
17 16 opeq2d 
 |-  ( q = Y -> <. ( F ` p ) , ( F ` q ) >. = <. ( F ` p ) , ( F ` Y ) >. )
18 oveq2 
 |-  ( q = Y -> ( p .x. q ) = ( p .x. Y ) )
19 18 fveq2d 
 |-  ( q = Y -> ( F ` ( p .x. q ) ) = ( F ` ( p .x. Y ) ) )
20 17 19 opeq12d 
 |-  ( q = Y -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. = <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. )
21 20 sneqd 
 |-  ( q = Y -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } = { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } )
22 21 ssiun2s 
 |-  ( Y e. V -> { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
23 22 ralrimivw 
 |-  ( Y e. V -> A. p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
24 ss2iun 
 |-  ( A. p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
25 23 24 syl 
 |-  ( Y e. V -> U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
26 25 3ad2ant3 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
27 15 26 sstrd 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
28 3 3ad2ant1 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
29 27 28 sseqtrrd 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ .xb )
30 opex 
 |-  <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. _V
31 30 snss 
 |-  ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb <-> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ .xb )
32 29 31 sylibr 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb )
33 funopfv 
 |-  ( Fun .xb -> ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb -> ( .xb ` <. ( F ` X ) , ( F ` Y ) >. ) = ( F ` ( X .x. Y ) ) ) )
34 8 32 33 sylc 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( .xb ` <. ( F ` X ) , ( F ` Y ) >. ) = ( F ` ( X .x. Y ) ) )
35 4 34 eqtrid 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )