lfladd0l

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

	Ref	Expression
Hypotheses	lfladd0l.v	$⊢ V = {Base}_{W}$
	lfladd0l.r	$⊢ R = Scalar (W)$
	lfladd0l.p	$⊢ \underset{˙}{+} = +_{R}$
	lfladd0l.o	$⊢ \underset{˙}{0} = 0_{R}$
	lfladd0l.f	$⊢ F = LFnl (W)$
	lfladd0l.w	$⊢ φ \to W \in LMod$
	lfladd0l.g	$⊢ φ \to G \in F$
Assertion	lfladd0l	$⊢ φ \to (V \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} G = G$

Step	Hyp	Ref	Expression
1		lfladd0l.v	$⊢ V = {Base}_{W}$
2		lfladd0l.r	$⊢ R = Scalar (W)$
3		lfladd0l.p	$⊢ \underset{˙}{+} = +_{R}$
4		lfladd0l.o	$⊢ \underset{˙}{0} = 0_{R}$
5		lfladd0l.f	$⊢ F = LFnl (W)$
6		lfladd0l.w	$⊢ φ \to W \in LMod$
7		lfladd0l.g	$⊢ φ \to G \in F$
8	1	fvexi	$⊢ V \in V$
9	8	a1i	$⊢ φ \to V \in V$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	2 10 1 5	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ {Base}_{R}$
12	6 7 11	syl2anc	$⊢ φ \to G : V ⟶ {Base}_{R}$
13	4	fvexi	$⊢ \underset{˙}{0} \in V$
14	13	a1i	$⊢ φ \to \underset{˙}{0} \in V$
15	2	lmodring	$⊢ W \in LMod \to R \in Ring$
16		ringgrp	$⊢ R \in Ring \to R \in Grp$
17	6 15 16	3syl	$⊢ φ \to R \in Grp$
18	10 3 4	grplid	$⊢ (R \in Grp \land k \in {Base}_{R}) \to \underset{˙}{0} \underset{˙}{+} k = k$
19	17 18	sylan	$⊢ (φ \land k \in {Base}_{R}) \to \underset{˙}{0} \underset{˙}{+} k = k$
20	9 12 14 19	caofid0l	$⊢ φ \to (V \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} G = G$

Metamath Proof Explorer