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 ( ( 𝜑𝑋𝐾𝑌𝑉 ) → ( 𝑋 ( 𝐹𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )