This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasvscaval

Description: The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasvscaf.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasvscaf.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasvscaf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasvscaf.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasvscaf.g ⊢ 𝐺 = ( Scalar ‘ 𝑅 )
imasvscaf.k ⊢ 𝐾 = ( Base ‘ 𝐺 )
imasvscaf.q ⊢ · = ( ·𝑠 ‘ 𝑅 )
imasvscaf.s ⊢ ∙ = ( ·𝑠 ‘ 𝑈 )
imasvscaf.e ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
Assertion imasvscaval ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 imasvscaf.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasvscaf.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasvscaf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4 imasvscaf.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasvscaf.g ⊢ 𝐺 = ( Scalar ‘ 𝑅 )
6 imasvscaf.k ⊢ 𝐾 = ( Base ‘ 𝐺 )
7 imasvscaf.q ⊢ · = ( ·𝑠 ‘ 𝑅 )
8 imasvscaf.s ⊢ ∙ = ( ·𝑠 ‘ 𝑈 )
9 imasvscaf.e ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
10 1 2 3 4 5 6 7 8 9 imasvscafn ⊢ ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) )
11 fnfun ⊢ ( ∙ Fn ( 𝐾 × 𝐵 ) → Fun ∙ )
12 10 11 syl ⊢ ( 𝜑 → Fun ∙ )
13 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → Fun ∙ )
14 eqidd ⊢ ( 𝑞 = 𝑌 → 𝐾 = 𝐾 )
15 fveq2 ⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑌 ) )
16 15 sneqd ⊢ ( 𝑞 = 𝑌 → { ( 𝐹 ‘ 𝑞 ) } = { ( 𝐹 ‘ 𝑌 ) } )
17 oveq2 ⊢ ( 𝑞 = 𝑌 → ( 𝑝 · 𝑞 ) = ( 𝑝 · 𝑌 ) )
18 17 fveq2d ⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) )
19 14 16 18 mpoeq123dv ⊢ ( 𝑞 = 𝑌 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) )
20 19 ssiun2s ⊢ ( 𝑌 ∈ 𝑉 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
21 20 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
22 1 2 3 4 5 6 7 8 imasvsca ⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
23 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
24 21 23 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ )
25 simp2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐾 )
26 fvex ⊢ ( 𝐹 ‘ 𝑌 ) ∈ V
27 26 snid ⊢ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) }
28 opelxpi ⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) )
29 25 27 28 sylancl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) )
30 eqid ⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) )
31 fvex ⊢ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ∈ V
32 30 31 dmmpo ⊢ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } )
33 29 32 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) )
34 funssfv ⊢ ( ( Fun ∙ ∧ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ ∧ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ) → ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) )
35 13 24 33 34 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) )
36 df-ov ⊢ ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ )
37 df-ov ⊢ ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ )
38 35 36 37 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) )
39 fvoveq1 ⊢ ( 𝑝 = 𝑋 → ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
40 eqidd ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑌 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
41 fvex ⊢ ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ∈ V
42 39 40 30 41 ovmpo ⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
43 25 27 42 sylancl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
44 38 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )