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

Metamath Proof Explorer

Theorem lfl1sc

Description: The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses lfl1sc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfl1sc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lfl1sc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfl1sc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lfl1sc.t ⊢ · = ( .r ‘ 𝐷 )
lfl1sc.i ⊢ 1 = ( 1r ‘ 𝐷 )
lfl1sc.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lfl1sc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lfl1sc ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 1 } ) ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 lfl1sc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lfl1sc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lfl1sc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lfl1sc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
5 lfl1sc.t ⊢ · = ( .r ‘ 𝐷 )
6 lfl1sc.i ⊢ 1 = ( 1r ‘ 𝐷 )
7 lfl1sc.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 lfl1sc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 1 fvexi ⊢ 𝑉 ∈ V
10 9 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
11 2 4 1 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
12 7 8 11 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
13 6 fvexi ⊢ 1 ∈ V
14 13 a1i ⊢ ( 𝜑 → 1 ∈ V )
15 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
16 7 15 syl ⊢ ( 𝜑 → 𝐷 ∈ Ring )
17 4 5 6 ringridm ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 1 ) = 𝑘 )
18 16 17 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 1 ) = 𝑘 )
19 10 12 14 18 caofid0r ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 1 } ) ) = 𝐺 )