ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasaddvallemg GIF version

Theorem imasaddvallemg 12742
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 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
imasaddfnlemg.v (𝜑𝑉𝑊)
imasaddfnlemg.x (𝜑·𝐶)
Assertion
Ref Expression
imasaddvallemg ((𝜑𝑋𝑉𝑌𝑉) → ((𝐹𝑋) (𝐹𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Distinct variable groups:   𝑞,𝑝,𝐵   𝑎,𝑏,𝑝,𝑞,𝑉   · ,𝑝,𝑞   𝑋,𝑝   𝐹,𝑎,𝑏,𝑝,𝑞   𝜑,𝑎,𝑏,𝑝,𝑞   ,𝑎,𝑏,𝑝,𝑞   𝑌,𝑝,𝑞
Allowed substitution hints:   𝐵(𝑎,𝑏)   𝐶(𝑞,𝑝,𝑎,𝑏)   · (𝑎,𝑏)   𝑊(𝑞,𝑝,𝑎,𝑏)   𝑋(𝑞,𝑎,𝑏)   𝑌(𝑎,𝑏)

Proof of Theorem imasaddvallemg
StepHypRef Expression
1 df-ov 5881 . 2 ((𝐹𝑋) (𝐹𝑌)) = ( ‘⟨(𝐹𝑋), (𝐹𝑌)⟩)
2 imasaddf.f . . . . . 6 (𝜑𝐹:𝑉onto𝐵)
3 imasaddf.e . . . . . 6 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
4 imasaddflem.a . . . . . 6 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
5 imasaddfnlemg.v . . . . . 6 (𝜑𝑉𝑊)
6 imasaddfnlemg.x . . . . . 6 (𝜑·𝐶)
72, 3, 4, 5, 6imasaddfnlemg 12741 . . . . 5 (𝜑 Fn (𝐵 × 𝐵))
8 fnfun 5315 . . . . 5 ( Fn (𝐵 × 𝐵) → Fun )
97, 8syl 14 . . . 4 (𝜑 → Fun )
1093ad2ant1 1018 . . 3 ((𝜑𝑋𝑉𝑌𝑉) → Fun )
11 fveq2 5517 . . . . . . . . . . 11 (𝑝 = 𝑋 → (𝐹𝑝) = (𝐹𝑋))
1211opeq1d 3786 . . . . . . . . . 10 (𝑝 = 𝑋 → ⟨(𝐹𝑝), (𝐹𝑌)⟩ = ⟨(𝐹𝑋), (𝐹𝑌)⟩)
13 fvoveq1 5901 . . . . . . . . . 10 (𝑝 = 𝑋 → (𝐹‘(𝑝 · 𝑌)) = (𝐹‘(𝑋 · 𝑌)))
1412, 13opeq12d 3788 . . . . . . . . 9 (𝑝 = 𝑋 → ⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩ = ⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩)
1514sneqd 3607 . . . . . . . 8 (𝑝 = 𝑋 → {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} = {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩})
1615ssiun2s 3932 . . . . . . 7 (𝑋𝑉 → {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ 𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩})
17163ad2ant2 1019 . . . . . 6 ((𝜑𝑋𝑉𝑌𝑉) → {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ 𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩})
18 fveq2 5517 . . . . . . . . . . . . 13 (𝑞 = 𝑌 → (𝐹𝑞) = (𝐹𝑌))
1918opeq2d 3787 . . . . . . . . . . . 12 (𝑞 = 𝑌 → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑌)⟩)
20 oveq2 5886 . . . . . . . . . . . . 13 (𝑞 = 𝑌 → (𝑝 · 𝑞) = (𝑝 · 𝑌))
2120fveq2d 5521 . . . . . . . . . . . 12 (𝑞 = 𝑌 → (𝐹‘(𝑝 · 𝑞)) = (𝐹‘(𝑝 · 𝑌)))
2219, 21opeq12d 3788 . . . . . . . . . . 11 (𝑞 = 𝑌 → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩)
2322sneqd 3607 . . . . . . . . . 10 (𝑞 = 𝑌 → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩})
2423ssiun2s 3932 . . . . . . . . 9 (𝑌𝑉 → {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
2524ralrimivw 2551 . . . . . . . 8 (𝑌𝑉 → ∀𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
26 ss2iun 3903 . . . . . . . 8 (∀𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
2725, 26syl 14 . . . . . . 7 (𝑌𝑉 𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
28273ad2ant3 1020 . . . . . 6 ((𝜑𝑋𝑉𝑌𝑉) → 𝑝𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑌)⟩, (𝐹‘(𝑝 · 𝑌))⟩} ⊆ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
2917, 28sstrd 3167 . . . . 5 ((𝜑𝑋𝑉𝑌𝑉) → {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
3043ad2ant1 1018 . . . . 5 ((𝜑𝑋𝑉𝑌𝑉) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
3129, 30sseqtrrd 3196 . . . 4 ((𝜑𝑋𝑉𝑌𝑉) → {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ )
32 fof 5440 . . . . . . . . . . 11 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
332, 32syl 14 . . . . . . . . . 10 (𝜑𝐹:𝑉𝐵)
34333ad2ant1 1018 . . . . . . . . 9 ((𝜑𝑋𝑉𝑌𝑉) → 𝐹:𝑉𝐵)
3553ad2ant1 1018 . . . . . . . . 9 ((𝜑𝑋𝑉𝑌𝑉) → 𝑉𝑊)
3634, 35fexd 5749 . . . . . . . 8 ((𝜑𝑋𝑉𝑌𝑉) → 𝐹 ∈ V)
37 simp2 998 . . . . . . . 8 ((𝜑𝑋𝑉𝑌𝑉) → 𝑋𝑉)
38 fvexg 5536 . . . . . . . 8 ((𝐹 ∈ V ∧ 𝑋𝑉) → (𝐹𝑋) ∈ V)
3936, 37, 38syl2anc 411 . . . . . . 7 ((𝜑𝑋𝑉𝑌𝑉) → (𝐹𝑋) ∈ V)
40 simp3 999 . . . . . . . 8 ((𝜑𝑋𝑉𝑌𝑉) → 𝑌𝑉)
41 fvexg 5536 . . . . . . . 8 ((𝐹 ∈ V ∧ 𝑌𝑉) → (𝐹𝑌) ∈ V)
4236, 40, 41syl2anc 411 . . . . . . 7 ((𝜑𝑋𝑉𝑌𝑉) → (𝐹𝑌) ∈ V)
43 opexg 4230 . . . . . . 7 (((𝐹𝑋) ∈ V ∧ (𝐹𝑌) ∈ V) → ⟨(𝐹𝑋), (𝐹𝑌)⟩ ∈ V)
4439, 42, 43syl2anc 411 . . . . . 6 ((𝜑𝑋𝑉𝑌𝑉) → ⟨(𝐹𝑋), (𝐹𝑌)⟩ ∈ V)
4563ad2ant1 1018 . . . . . . . 8 ((𝜑𝑋𝑉𝑌𝑉) → ·𝐶)
46 ovexg 5912 . . . . . . . 8 ((𝑋𝑉·𝐶𝑌𝑉) → (𝑋 · 𝑌) ∈ V)
4737, 45, 40, 46syl3anc 1238 . . . . . . 7 ((𝜑𝑋𝑉𝑌𝑉) → (𝑋 · 𝑌) ∈ V)
48 fvexg 5536 . . . . . . 7 ((𝐹 ∈ V ∧ (𝑋 · 𝑌) ∈ V) → (𝐹‘(𝑋 · 𝑌)) ∈ V)
4936, 47, 48syl2anc 411 . . . . . 6 ((𝜑𝑋𝑉𝑌𝑉) → (𝐹‘(𝑋 · 𝑌)) ∈ V)
50 opexg 4230 . . . . . 6 ((⟨(𝐹𝑋), (𝐹𝑌)⟩ ∈ V ∧ (𝐹‘(𝑋 · 𝑌)) ∈ V) → ⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ V)
5144, 49, 50syl2anc 411 . . . . 5 ((𝜑𝑋𝑉𝑌𝑉) → ⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ V)
52 snssg 3728 . . . . 5 (⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ V → (⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ ↔ {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ ))
5351, 52syl 14 . . . 4 ((𝜑𝑋𝑉𝑌𝑉) → (⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ ↔ {⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩} ⊆ ))
5431, 53mpbird 167 . . 3 ((𝜑𝑋𝑉𝑌𝑉) → ⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ )
55 funopfv 5558 . . 3 (Fun → (⟨⟨(𝐹𝑋), (𝐹𝑌)⟩, (𝐹‘(𝑋 · 𝑌))⟩ ∈ → ( ‘⟨(𝐹𝑋), (𝐹𝑌)⟩) = (𝐹‘(𝑋 · 𝑌))))
5610, 54, 55sylc 62 . 2 ((𝜑𝑋𝑉𝑌𝑉) → ( ‘⟨(𝐹𝑋), (𝐹𝑌)⟩) = (𝐹‘(𝑋 · 𝑌)))
571, 56eqtrid 2222 1 ((𝜑𝑋𝑉𝑌𝑉) → ((𝐹𝑋) (𝐹𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  wral 2455  Vcvv 2739  wss 3131  {csn 3594  cop 3597   ciun 3888   × cxp 4626  Fun wfun 5212   Fn wfn 5213  wf 5214  ontowfo 5216  cfv 5218  (class class class)co 5878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5881
This theorem is referenced by:  imasaddval  12745  imasmulval  12748  qusaddvallemg  12758
  Copyright terms: Public domain W3C validator