MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasaddvallem Structured version   Visualization version   GIF version

Theorem imasaddvallem 17502
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 (๐œ‘ โ†’ ๐น:๐‘‰โ€“ontoโ†’๐ต)
imasaddf.e ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž)) โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
imasaddflem.a (๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
Assertion
Ref Expression
imasaddvallem ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
Distinct variable groups:   ๐‘ž,๐‘,๐ต   ๐‘Ž,๐‘,๐‘,๐‘ž,๐‘‰   ยท ,๐‘,๐‘ž   ๐‘‹,๐‘   ๐น,๐‘Ž,๐‘,๐‘,๐‘ž   ๐œ‘,๐‘Ž,๐‘,๐‘,๐‘ž   โˆ™ ,๐‘Ž,๐‘,๐‘,๐‘ž   ๐‘Œ,๐‘,๐‘ž
Allowed substitution hints:   ๐ต(๐‘Ž,๐‘)   ยท (๐‘Ž,๐‘)   ๐‘‹(๐‘ž,๐‘Ž,๐‘)   ๐‘Œ(๐‘Ž,๐‘)

Proof of Theorem imasaddvallem
StepHypRef Expression
1 df-ov 7417 . 2 ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ)
2 imasaddf.f . . . . . 6 (๐œ‘ โ†’ ๐น:๐‘‰โ€“ontoโ†’๐ต)
3 imasaddf.e . . . . . 6 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž)) โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
4 imasaddflem.a . . . . . 6 (๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
52, 3, 4imasaddfnlem 17501 . . . . 5 (๐œ‘ โ†’ โˆ™ Fn (๐ต ร— ๐ต))
6 fnfun 6648 . . . . 5 ( โˆ™ Fn (๐ต ร— ๐ต) โ†’ Fun โˆ™ )
75, 6syl 17 . . . 4 (๐œ‘ โ†’ Fun โˆ™ )
873ad2ant1 1131 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ Fun โˆ™ )
9 fveq2 6891 . . . . . . . . . . 11 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜๐‘) = (๐นโ€˜๐‘‹))
109opeq1d 4875 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ = โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ)
11 fvoveq1 7437 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜(๐‘ ยท ๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
1210, 11opeq12d 4877 . . . . . . . . 9 (๐‘ = ๐‘‹ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ)
1312sneqd 4636 . . . . . . . 8 (๐‘ = ๐‘‹ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ})
1413ssiun2s 5045 . . . . . . 7 (๐‘‹ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
15143ad2ant2 1132 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
16 fveq2 6891 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜๐‘ž) = (๐นโ€˜๐‘Œ))
1716opeq2d 4876 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ)
18 oveq2 7422 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐‘ ยท ๐‘ž) = (๐‘ ยท ๐‘Œ))
1918fveq2d 6895 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) = (๐นโ€˜(๐‘ ยท ๐‘Œ)))
2017, 19opeq12d 4877 . . . . . . . . . . 11 (๐‘ž = ๐‘Œ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ)
2120sneqd 4636 . . . . . . . . . 10 (๐‘ž = ๐‘Œ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
2221ssiun2s 5045 . . . . . . . . 9 (๐‘Œ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2322ralrimivw 3145 . . . . . . . 8 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
24 ss2iun 5009 . . . . . . . 8 (โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2523, 24syl 17 . . . . . . 7 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
26253ad2ant3 1133 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2715, 26sstrd 3988 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2843ad2ant1 1131 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2927, 28sseqtrrd 4019 . . . 4 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ )
30 opex 5460 . . . . 5 โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V
3130snss 4785 . . . 4 (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ )
3229, 31sylibr 233 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ )
33 funopfv 6943 . . 3 (Fun โˆ™ โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ))))
348, 32, 33sylc 65 . 2 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
351, 34eqtrid 2779 1 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099  โˆ€wral 3056   โІ wss 3944  {csn 4624  โŸจcop 4630  โˆช ciun 4991   ร— cxp 5670  Fun wfun 6536   Fn wfn 6537  โ€“ontoโ†’wfo 6540  โ€˜cfv 6542  (class class class)co 7414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fo 6548  df-fv 6550  df-ov 7417
This theorem is referenced by:  imasaddval  17505  imasmulval  17508  qusaddvallem  17524
  Copyright terms: Public domain W3C validator