Metamath Proof Explorer


Theorem imasvsca

Description: The scalar multiplication operation of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses imasbas.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasbas.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasbas.r ( 𝜑𝑅𝑍 )
imassca.g 𝐺 = ( Scalar ‘ 𝑅 )
imasvsca.k 𝐾 = ( Base ‘ 𝐺 )
imasvsca.q · = ( ·𝑠𝑅 )
imasvsca.s = ( ·𝑠𝑈 )
Assertion imasvsca ( 𝜑 = 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )

Proof

Step Hyp Ref Expression
1 imasbas.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
2 imasbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 imasbas.f ( 𝜑𝐹 : 𝑉onto𝐵 )
4 imasbas.r ( 𝜑𝑅𝑍 )
5 imassca.g 𝐺 = ( Scalar ‘ 𝑅 )
6 imasvsca.k 𝐾 = ( Base ‘ 𝐺 )
7 imasvsca.q · = ( ·𝑠𝑅 )
8 imasvsca.s = ( ·𝑠𝑈 )
9 eqid ( +g𝑅 ) = ( +g𝑅 )
10 eqid ( .r𝑅 ) = ( .r𝑅 )
11 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
12 5 fveq2i ( Base ‘ 𝐺 ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
13 6 12 eqtri 𝐾 = ( Base ‘ ( Scalar ‘ 𝑅 ) )
14 eqid ( ·𝑖𝑅 ) = ( ·𝑖𝑅 )
15 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
16 eqid ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
17 eqid ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
18 eqid ( +g𝑈 ) = ( +g𝑈 )
19 1 2 3 4 9 18 imasplusg ( 𝜑 → ( +g𝑈 ) = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } )
20 eqid ( .r𝑈 ) = ( .r𝑈 )
21 1 2 3 4 10 20 imasmulr ( 𝜑 → ( .r𝑈 ) = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } )
22 eqidd ( 𝜑 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
23 eqidd ( 𝜑 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } )
24 eqidd ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
25 eqid ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
26 1 2 3 4 16 25 imasds ( 𝜑 → ( dist ‘ 𝑈 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑢 ∈ ℕ ran ( 𝑧 ∈ { 𝑤 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑢 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( 𝑤 ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑤𝑢 ) ) ) = 𝑦 ∧ ∀ 𝑣 ∈ ( 1 ... ( 𝑢 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑤𝑣 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( 𝑤 ‘ ( 𝑣 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑧 ) ) ) , ℝ* , < ) ) )
27 eqidd ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) )
28 1 2 9 10 11 13 7 14 15 16 17 19 21 22 23 24 26 27 3 4 imasval ( 𝜑𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) )
29 eqid ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
30 29 imasvalstr ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) Struct ⟨ 1 , 1 2 ⟩
31 vscaid ·𝑠 = Slot ( ·𝑠 ‘ ndx )
32 snsstp2 { ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ } ⊆ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ }
33 ssun2 { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } )
34 ssun1 ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
35 33 34 sstri { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
36 32 35 sstri { ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
37 fvex ( Base ‘ 𝑅 ) ∈ V
38 2 37 eqeltrdi ( 𝜑𝑉 ∈ V )
39 6 fvexi 𝐾 ∈ V
40 snex { ( 𝐹𝑞 ) } ∈ V
41 39 40 mpoex ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V
42 41 rgenw 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V
43 iunexg ( ( 𝑉 ∈ V ∧ ∀ 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V ) → 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V )
44 38 42 43 sylancl ( 𝜑 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ∈ V )
45 28 30 31 36 44 8 strfv3 ( 𝜑 = 𝑞𝑉 ( 𝑝𝐾 , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )