ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasaddvallemg Unicode version
Theorem imasaddvallemg 13636
Description: The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
Hypotheses
Ref Expression
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 ) ) >. } )
imasaddfnlemg.v |- ( ph -> V e. W )
imasaddfnlemg.x |- ( ph -> .x. e. C )
Assertion
Ref Expression
imasaddvallemg |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Distinct variable groups:   q, p, B   a, b, p, q, V   .x. , p, q   X, p   F, a, b, p, q   ph, a, b, p, q   .xb , a, b, p, q   Y, p, q
Allowed substitution hints:   B( a, b)   C( q, p, a, b)   .x. ( a, b)   W( q, p, a, b)   X( q, a, b)   Y( a, b)
Proof of Theorem imasaddvallemg
StepHypRef Expression
1 df-ov 6088 . 2 |- ( ( F ` X ) .xb ( F ` Y ) ) = ( .xb ` <. ( F ` X ) , ( F ` Y ) >. )
2 imasaddf.f . . . . . 6 |- ( ph -> F : V -onto-> B )
3 imasaddf.e . . . . . 6 |- ( ( 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 ) ) ) )
4 imasaddflem.a . . . . . 6 |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
5 imasaddfnlemg.v . . . . . 6 |- ( ph -> V e. W )
6 imasaddfnlemg.x . . . . . 6 |- ( ph -> .x. e. C )
72, 3, 4, 5, 6imasaddfnlemg 13635 . . . . 5 |- ( ph -> .xb Fn ( B X. B ) )
8 fnfun 5478 . . . . 5 |- ( .xb Fn ( B X. B ) -> Fun .xb )
97, 8syl 14 . . . 4 |- ( ph -> Fun .xb )
1093ad2ant1 1049 . . 3 |- ( ( ph /\ X e. V /\ Y e. V ) -> Fun .xb )
11 fveq2 5695 . . . . . . . . . . 11 |- ( p = X -> ( F ` p ) = ( F ` X ) )
1211opeq1d 3910 . . . . . . . . . 10 |- ( p = X -> <. ( F ` p ) , ( F ` Y ) >. = <. ( F ` X ) , ( F ` Y ) >. )
13 fvoveq1 6108 . . . . . . . . . 10 |- ( p = X -> ( F ` ( p .x. Y ) ) = ( F ` ( X .x. Y ) ) )
1412, 13opeq12d 3912 . . . . . . . . 9 |- ( p = X -> <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. = <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. )
1514sneqd 3722 . . . . . . . 8 |- ( p = X -> { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } = { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } )
1615ssiun2s 4056 . . . . . . 7 |- ( X e. V -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ U_ p e. V { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } )
17163ad2ant2 1050 . . . . . 6 |- ( ( 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 ) ) >. } )
18 fveq2 5695 . . . . . . . . . . . . 13 |- ( q = Y -> ( F ` q ) = ( F ` Y ) )
1918opeq2d 3911 . . . . . . . . . . . 12 |- ( q = Y -> <. ( F ` p ) , ( F ` q ) >. = <. ( F ` p ) , ( F ` Y ) >. )
20 oveq2 6093 . . . . . . . . . . . . 13 |- ( q = Y -> ( p .x. q ) = ( p .x. Y ) )
2120fveq2d 5699 . . . . . . . . . . . 12 |- ( q = Y -> ( F ` ( p .x. q ) ) = ( F ` ( p .x. Y ) ) )
2219, 21opeq12d 3912 . . . . . . . . . . 11 |- ( q = Y -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. = <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. )
2322sneqd 3722 . . . . . . . . . 10 |- ( q = Y -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } = { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } )
2423ssiun2s 4056 . . . . . . . . 9 |- ( Y e. V -> { <. <. ( F ` p ) , ( F ` Y ) >. , ( F ` ( p .x. Y ) ) >. } C_ U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
2524ralrimivw 2624 . . . . . . . 8 |- ( 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 ) ) >. } )
26 ss2iun 4027 . . . . . . . 8 |- ( 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 ) ) >. } )
2725, 26syl 14 . . . . . . 7 |- ( 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 ) ) >. } )
28273ad2ant3 1051 . . . . . 6 |- ( ( 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 ) ) >. } )
2917, 28sstrd 3258 . . . . 5 |- ( ( 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 ) ) >. } )
3043ad2ant1 1049 . . . . 5 |- ( ( ph /\ X e. V /\ Y e. V ) -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
3129, 30sseqtrrd 3287 . . . 4 |- ( ( ph /\ X e. V /\ Y e. V ) -> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ .xb )
32 fof 5615 . . . . . . . . . . 11 |- ( F : V -onto-> B -> F : V --> B )
332, 32syl 14 . . . . . . . . . 10 |- ( ph -> F : V --> B )
34333ad2ant1 1049 . . . . . . . . 9 |- ( ( ph /\ X e. V /\ Y e. V ) -> F : V --> B )
3553ad2ant1 1049 . . . . . . . . 9 |- ( ( ph /\ X e. V /\ Y e. V ) -> V e. W )
3634, 35fexd 5948 . . . . . . . 8 |- ( ( ph /\ X e. V /\ Y e. V ) -> F e. _V )
37 simp2 1029 . . . . . . . 8 |- ( ( ph /\ X e. V /\ Y e. V ) -> X e. V )
38 fvexg 5714 . . . . . . . 8 |- ( ( F e. _V /\ X e. V ) -> ( F ` X ) e. _V )
3936, 37, 38syl2anc 415 . . . . . . 7 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` X ) e. _V )
40 simp3 1030 . . . . . . . 8 |- ( ( ph /\ X e. V /\ Y e. V ) -> Y e. V )
41 fvexg 5714 . . . . . . . 8 |- ( ( F e. _V /\ Y e. V ) -> ( F ` Y ) e. _V )
4236, 40, 41syl2anc 415 . . . . . . 7 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` Y ) e. _V )
43 opexg 4368 . . . . . . 7 |- ( ( ( F ` X ) e. _V /\ ( F ` Y ) e. _V ) -> <. ( F ` X ) , ( F ` Y ) >. e. _V )
4439, 42, 43syl2anc 415 . . . . . 6 |- ( ( ph /\ X e. V /\ Y e. V ) -> <. ( F ` X ) , ( F ` Y ) >. e. _V )
4563ad2ant1 1049 . . . . . . . 8 |- ( ( ph /\ X e. V /\ Y e. V ) -> .x. e. C )
46 ovexg 6119 . . . . . . . 8 |- ( ( X e. V /\ .x. e. C /\ Y e. V ) -> ( X .x. Y ) e. _V )
4737, 45, 40, 46syl3anc 1278 . . . . . . 7 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( X .x. Y ) e. _V )
48 fvexg 5714 . . . . . . 7 |- ( ( F e. _V /\ ( X .x. Y ) e. _V ) -> ( F ` ( X .x. Y ) ) e. _V )
4936, 47, 48syl2anc 415 . . . . . 6 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` ( X .x. Y ) ) e. _V )
50 opexg 4368 . . . . . 6 |- ( ( <. ( F ` X ) , ( F ` Y ) >. e. _V /\ ( F ` ( X .x. Y ) ) e. _V ) -> <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. _V )
5144, 49, 50syl2anc 415 . . . . 5 |- ( ( ph /\ X e. V /\ Y e. V ) -> <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. _V )
52 snssg 3849 . . . . 5 |- ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. _V -> ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb <-> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ .xb ) )
5351, 52syl 14 . . . 4 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb <-> { <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. } C_ .xb ) )
5431, 53mpbird 167 . . 3 |- ( ( ph /\ X e. V /\ Y e. V ) -> <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb )
55 funopfv 5740 . . 3 |- ( Fun .xb -> ( <. <. ( F ` X ) , ( F ` Y ) >. , ( F ` ( X .x. Y ) ) >. e. .xb -> ( .xb ` <. ( F ` X ) , ( F ` Y ) >. ) = ( F ` ( X .x. Y ) ) ) )
5610, 54, 55sylc 62 . 2 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( .xb ` <. ( F ` X ) , ( F ` Y ) >. ) = ( F ` ( X .x. Y ) ) )
571, 56eqtrid 2283 1 |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Colors of variables:    wff set class
This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   e. wcel 2209   A.wral 2528   _Vcvv 2821   C_ wss 3220   {csn 3709   <.cop 3712   U_ciun 4012   X. cxp 4772   Fun wfun 5371   Fn wfn 5372   -->wf 5373   -onto->wfo 5375   ` cfv 5377  (class class class)co 6085
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578
This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088
This theorem is used by:  imasaddval  13639  imasmulval  13642  qusaddvallemg  13654
  Copyright terms: Public domain W3C validator