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

Metamath Proof Explorer

Theorem lfladd0l

Description: Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses lfladd0l.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfladd0l.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
lfladd0l.p ⊢ + = ( +g ‘ 𝑅 )
lfladd0l.o ⊢ 0 = ( 0g ‘ 𝑅 )
lfladd0l.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfladd0l.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lfladd0l.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lfladd0l ( 𝜑 → ( ( 𝑉 × { 0 } ) ∘f + 𝐺 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 lfladd0l.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lfladd0l.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 lfladd0l.p ⊢ + = ( +g ‘ 𝑅 )
4 lfladd0l.o ⊢ 0 = ( 0g ‘ 𝑅 )
5 lfladd0l.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lfladd0l.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lfladd0l.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8 1 fvexi ⊢ 𝑉 ∈ V
9 8 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 2 10 1 5 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
12 6 7 11 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
13 4 fvexi ⊢ 0 ∈ V
14 13 a1i ⊢ ( 𝜑 → 0 ∈ V )
15 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
16 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
17 6 15 16 3syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
18 10 3 4 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ) → ( 0 + 𝑘 ) = 𝑘 )
19 17 18 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ) → ( 0 + 𝑘 ) = 𝑘 )
20 9 12 14 19 caofid0l ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ∘f + 𝐺 ) = 𝐺 )