lmhmplusg

Description: The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015)

		Ref	Expression
	Hypothesis	lmhmplusg.p	$⊢ \underset{˙}{+} = +_{N}$
	Assertion	lmhmplusg	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to F {\underset{˙}{+}}_{f} G \in (M LMHom N)$

Proof

Step	Hyp	Ref	Expression
1		lmhmplusg.p	$⊢ \underset{˙}{+} = +_{N}$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ \cdot_{M} = \cdot_{M}$
4		eqid	$⊢ \cdot_{N} = \cdot_{N}$
5		eqid	$⊢ Scalar (M) = Scalar (M)$
6		eqid	$⊢ Scalar (N) = Scalar (N)$
7		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
8		lmhmlmod1	$⊢ F \in (M LMHom N) \to M \in LMod$
9	8	adantr	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to M \in LMod$
10		lmhmlmod2	$⊢ F \in (M LMHom N) \to N \in LMod$
11	10	adantr	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to N \in LMod$
12	5 6	lmhmsca	$⊢ F \in (M LMHom N) \to Scalar (N) = Scalar (M)$
13	12	adantr	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to Scalar (N) = Scalar (M)$
14		lmodabl	$⊢ N \in LMod \to N \in Abel$
15	11 14	syl	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to N \in Abel$
16		lmghm	$⊢ F \in (M LMHom N) \to F \in (M GrpHom N)$
17	16	adantr	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to F \in (M GrpHom N)$
18		lmghm	$⊢ G \in (M LMHom N) \to G \in (M GrpHom N)$
19	18	adantl	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to G \in (M GrpHom N)$
20	1	ghmplusg	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to F {\underset{˙}{+}}_{f} G \in (M GrpHom N)$
21	15 17 19 20	syl3anc	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to F {\underset{˙}{+}}_{f} G \in (M GrpHom N)$
22		simpll	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F \in (M LMHom N)$
23		simprl	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \in {Base}_{Scalar (M)}$
24		simprr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to y \in {Base}_{M}$
25	5 7 2 3 4	lmhmlin	$⊢ (F \in (M LMHom N) \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to F (x \cdot_{M} y) = x \cdot_{N} F (y)$
26	22 23 24 25	syl3anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (x \cdot_{M} y) = x \cdot_{N} F (y)$
27		simplr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G \in (M LMHom N)$
28	5 7 2 3 4	lmhmlin	$⊢ (G \in (M LMHom N) \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to G (x \cdot_{M} y) = x \cdot_{N} G (y)$
29	27 23 24 28	syl3anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G (x \cdot_{M} y) = x \cdot_{N} G (y)$
30	26 29	oveq12d	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (x \cdot_{M} y) \underset{˙}{+} G (x \cdot_{M} y) = (x \cdot_{N} F (y)) \underset{˙}{+} (x \cdot_{N} G (y))$
31	10	ad2antrr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to N \in LMod$
32	12	fveq2d	$⊢ F \in (M LMHom N) \to {Base}_{Scalar (N)} = {Base}_{Scalar (M)}$
33	32	ad2antrr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to {Base}_{Scalar (N)} = {Base}_{Scalar (M)}$
34	23 33	eleqtrrd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \in {Base}_{Scalar (N)}$
35		eqid	$⊢ {Base}_{N} = {Base}_{N}$
36	2 35	lmhmf	$⊢ F \in (M LMHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
37	36	ad2antrr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F : {Base}_{M} ⟶ {Base}_{N}$
38	37 24	ffvelcdmd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (y) \in {Base}_{N}$
39	2 35	lmhmf	$⊢ G \in (M LMHom N) \to G : {Base}_{M} ⟶ {Base}_{N}$
40	39	ad2antlr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G : {Base}_{M} ⟶ {Base}_{N}$
41	40 24	ffvelcdmd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G (y) \in {Base}_{N}$
42		eqid	$⊢ {Base}_{Scalar (N)} = {Base}_{Scalar (N)}$
43	35 1 6 4 42	lmodvsdi	$⊢ (N \in LMod \land (x \in {Base}_{Scalar (N)} \land F (y) \in {Base}_{N} \land G (y) \in {Base}_{N})) \to x \cdot_{N} (F (y) \underset{˙}{+} G (y)) = (x \cdot_{N} F (y)) \underset{˙}{+} (x \cdot_{N} G (y))$
44	31 34 38 41 43	syl13anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \cdot_{N} (F (y) \underset{˙}{+} G (y)) = (x \cdot_{N} F (y)) \underset{˙}{+} (x \cdot_{N} G (y))$
45	30 44	eqtr4d	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (x \cdot_{M} y) \underset{˙}{+} G (x \cdot_{M} y) = x \cdot_{N} (F (y) \underset{˙}{+} G (y))$
46	37	ffnd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F Fn {Base}_{M}$
47	40	ffnd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G Fn {Base}_{M}$
48		fvexd	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to {Base}_{M} \in V$
49	8	ad2antrr	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to M \in LMod$
50	2 5 3 7	lmodvscl	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to x \cdot_{M} y \in {Base}_{M}$
51	49 23 24 50	syl3anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \cdot_{M} y \in {Base}_{M}$
52		fnfvof	$⊢ ((F Fn {Base}_{M} \land G Fn {Base}_{M}) \land ({Base}_{M} \in V \land x \cdot_{M} y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x \cdot_{M} y) = F (x \cdot_{M} y) \underset{˙}{+} G (x \cdot_{M} y)$
53	46 47 48 51 52	syl22anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x \cdot_{M} y) = F (x \cdot_{M} y) \underset{˙}{+} G (x \cdot_{M} y)$
54		fnfvof	$⊢ ((F Fn {Base}_{M} \land G Fn {Base}_{M}) \land ({Base}_{M} \in V \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (y) = F (y) \underset{˙}{+} G (y)$
55	46 47 48 24 54	syl22anc	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (y) = F (y) \underset{˙}{+} G (y)$
56	55	oveq2d	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \cdot_{N} (F {\underset{˙}{+}}_{f} G) (y) = x \cdot_{N} (F (y) \underset{˙}{+} G (y))$
57	45 53 56	3eqtr4d	$⊢ ((F \in (M LMHom N) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x \cdot_{M} y) = x \cdot_{N} (F {\underset{˙}{+}}_{f} G) (y)$
58	2 3 4 5 6 7 9 11 13 21 57	islmhmd	$⊢ (F \in (M LMHom N) \land G \in (M LMHom N)) \to F {\underset{˙}{+}}_{f} G \in (M LMHom N)$

Metamath Proof Explorer

Theorem lmhmplusg

Proof