Metamath Proof Explorer


Theorem imasvscaf

Description: The image structure's scalar multiplication is closed in the base set. (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 ( ( 𝜑 ∧ ( 𝑝𝐾𝑎𝑉𝑞𝑉 ) ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasvscaf.c ( ( 𝜑 ∧ ( 𝑝𝐾𝑞𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
Assertion imasvscaf ( 𝜑 : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )

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 imasvscaf.c ( ( 𝜑 ∧ ( 𝑝𝐾𝑞𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
11 1 2 3 4 5 6 7 8 9 imasvscafn ( 𝜑 Fn ( 𝐾 × 𝐵 ) )
12 1 2 3 4 5 6 7 8 imasvsca ( 𝜑 = 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
13 fof ( 𝐹 : 𝑉onto𝐵𝐹 : 𝑉𝐵 )
14 3 13 syl ( 𝜑𝐹 : 𝑉𝐵 )
15 14 ffvelrnda ( ( 𝜑 ∧ ( 𝑝 · 𝑞 ) ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
16 10 15 syldan ( ( 𝜑 ∧ ( 𝑝𝐾𝑞𝑉 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
17 16 ralrimivw ( ( 𝜑 ∧ ( 𝑝𝐾𝑞𝑉 ) ) → ∀ 𝑥 ∈ { ( 𝐹𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
18 17 anass1rs ( ( ( 𝜑𝑞𝑉 ) ∧ 𝑝𝐾 ) → ∀ 𝑥 ∈ { ( 𝐹𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
19 18 ralrimiva ( ( 𝜑𝑞𝑉 ) → ∀ 𝑝𝐾𝑥 ∈ { ( 𝐹𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
20 eqid ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
21 20 fmpo ( ∀ 𝑝𝐾𝑥 ∈ { ( 𝐹𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 ↔ ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹𝑞 ) } ) ⟶ 𝐵 )
22 19 21 sylib ( ( 𝜑𝑞𝑉 ) → ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹𝑞 ) } ) ⟶ 𝐵 )
23 fssxp ( ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹𝑞 ) } ) ⟶ 𝐵 → ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹𝑞 ) } ) × 𝐵 ) )
24 22 23 syl ( ( 𝜑𝑞𝑉 ) → ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹𝑞 ) } ) × 𝐵 ) )
25 14 ffvelrnda ( ( 𝜑𝑞𝑉 ) → ( 𝐹𝑞 ) ∈ 𝐵 )
26 25 snssd ( ( 𝜑𝑞𝑉 ) → { ( 𝐹𝑞 ) } ⊆ 𝐵 )
27 xpss2 ( { ( 𝐹𝑞 ) } ⊆ 𝐵 → ( 𝐾 × { ( 𝐹𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) )
28 xpss1 ( ( 𝐾 × { ( 𝐹𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) → ( ( 𝐾 × { ( 𝐹𝑞 ) } ) × 𝐵 ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
29 26 27 28 3syl ( ( 𝜑𝑞𝑉 ) → ( ( 𝐾 × { ( 𝐹𝑞 ) } ) × 𝐵 ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
30 24 29 sstrd ( ( 𝜑𝑞𝑉 ) → ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
31 30 ralrimiva ( 𝜑 → ∀ 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
32 iunss ( 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) ↔ ∀ 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
33 31 32 sylibr ( 𝜑 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
34 12 33 eqsstrd ( 𝜑 ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
35 dff2 ( : ( 𝐾 × 𝐵 ) ⟶ 𝐵 ↔ ( Fn ( 𝐾 × 𝐵 ) ∧ ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) ) )
36 11 34 35 sylanbrc ( 𝜑 : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )