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

Metamath Proof Explorer

Theorem lfladd

Description: Property of a linear functional. ( lnfnaddi analog.) (Contributed by NM, 18-Apr-2014)

Ref Expression
Hypotheses lfladd.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lfladd.p ⊢ ⨣ = ( +g ‘ 𝐷 )
lfladd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfladd.a ⊢ + = ( +g ‘ 𝑊 )
lfladd.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lfladd ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lfladd.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lfladd.p ⊢ ⨣ = ( +g ‘ 𝐷 )
3 lfladd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lfladd.a ⊢ + = ( +g ‘ 𝑊 )
5 lfladd.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
7 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 )
8 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9 eqid ⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 )
10 1 8 9 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) )
11 10 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) )
12 simp3l ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑋 ∈ 𝑉 )
13 simp3r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑌 ∈ 𝑉 )
14 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
15 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
16 3 4 1 14 8 2 15 5 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) ) = ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )
17 6 7 11 12 13 16 syl113anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) ) = ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )
18 3 1 14 9 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
19 6 12 18 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
20 19 fvoveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 + 𝑌 ) ) )
21 1 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
22 21 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐷 ∈ Ring )
23 1 8 3 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
24 23 3adant3r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
25 8 15 9 ringlidm ⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( 𝐺 ‘ 𝑋 ) )
26 22 24 25 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( 𝐺 ‘ 𝑋 ) )
27 26 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )
28 17 20 27 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )