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 + 𝐺 ) = 𝐺 )