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

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝑝 · 𝑞 ) ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 )
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 ⊢ ( 𝜑 → ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )