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 ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
Assertion imasaddvallem ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
2 imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
3 imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
4 df-ov ⊢ ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( ∙ ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ )
5 1 2 3 imasaddfnlem ⊢ ( 𝜑 → ∙ Fn ( 𝐵 × 𝐵 ) )
6 fnfun ⊢ ( ∙ Fn ( 𝐵 × 𝐵 ) → Fun ∙ )
7 5 6 syl ⊢ ( 𝜑 → Fun ∙ )
8 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → Fun ∙ )
9 fveq2 ⊢ ( 𝑝 = 𝑋 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑋 ) )
10 9 opeq1d ⊢ ( 𝑝 = 𝑋 → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ )
11 fvoveq1 ⊢ ( 𝑝 = 𝑋 → ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
12 10 11 opeq12d ⊢ ( 𝑝 = 𝑋 → ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ = ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ )
13 12 sneqd ⊢ ( 𝑝 = 𝑋 → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } = { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } )
14 13 ssiun2s ⊢ ( 𝑋 ∈ 𝑉 → { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } )
15 14 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } )
16 fveq2 ⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑌 ) )
17 16 opeq2d ⊢ ( 𝑞 = 𝑌 → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ )
18 oveq2 ⊢ ( 𝑞 = 𝑌 → ( 𝑝 · 𝑞 ) = ( 𝑝 · 𝑌 ) )
19 18 fveq2d ⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) )
20 17 19 opeq12d ⊢ ( 𝑞 = 𝑌 → ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ = ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ )
21 20 sneqd ⊢ ( 𝑞 = 𝑌 → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } = { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } )
22 21 ssiun2s ⊢ ( 𝑌 ∈ 𝑉 → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
23 22 ralrimivw ⊢ ( 𝑌 ∈ 𝑉 → ∀ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
24 ss2iun ⊢ ( ∀ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } → ∪ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
25 23 24 syl ⊢ ( 𝑌 ∈ 𝑉 → ∪ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
26 25 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ∪ 𝑝 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
27 15 26 sstrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } ⊆ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
28 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
29 27 28 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } ⊆ ∙ )
30 opex ⊢ ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ ∈ V
31 30 snss ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ ∈ ∙ ↔ { ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ } ⊆ ∙ )
32 29 31 sylibr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ ∈ ∙ )
33 funopfv ⊢ ( Fun ∙ → ( ⟨ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ , ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ⟩ ∈ ∙ → ( ∙ ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) )
34 8 32 33 sylc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ∙ ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
35 4 34 syl5eq ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )