Theorem lmhmplusg

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

	Ref	Expression
Hypothesis	lmhmplusg.p	⊢ + = ( +g ‘ 𝑁 )
Assertion	lmhmplusg	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 LMHom 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		lmhmplusg.p	⊢ + = ( +g ‘ 𝑁 )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
4		eqid	⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 )
5		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
6		eqid	⊢ ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑁 )
7		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8		lmhmlmod1	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑀 ∈ LMod )
9	8	adantr	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑀 ∈ LMod )
10		lmhmlmod2	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑁 ∈ LMod )
11	10	adantr	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑁 ∈ LMod )
12	5 6	lmhmsca	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) )
13	12	adantr	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) )
14		lmodabl	⊢ ( 𝑁 ∈ LMod → 𝑁 ∈ Abel )
15	11 14	syl	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑁 ∈ Abel )
16		lmghm	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
17	16	adantr	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
18		lmghm	⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) )
19	18	adantl	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) )
20	1	ghmplusg	⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
21	15 17 19 20	syl3anc	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
22		simpll	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) )
23		simprl	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
24		simprr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
25	5 7 2 3 4	lmhmlin	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) )
26	22 23 24 25	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) )
27		simplr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) )
28	5 7 2 3 4	lmhmlin	⊢ ( ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
29	27 23 24 28	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
30	26 29	oveq12d	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
31	10	ad2antrr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑁 ∈ LMod )
32	12	fveq2d	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
33	32	ad2antrr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
34	23 33	eleqtrrd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) )
35		eqid	⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
36	2 35	lmhmf	⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
37	36	ad2antrr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
38	37 24	ffvelcdmd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
39	2 35	lmhmf	⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
40	39	ad2antlr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
41	40 24	ffvelcdmd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
42		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑁 ) )
43	35 1 6 4 42	lmodvsdi	⊢ ( ( 𝑁 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
44	31 34 38 41 43	syl13anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
45	30 44	eqtr4d	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
46	37	ffnd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
47	40	ffnd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) )
48		fvexd	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ 𝑀 ) ∈ V )
49	8	ad2antrr	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
50	2 5 3 7	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
51	49 23 24 50	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
52		fnfvof	⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
53	46 47 48 51 52	syl22anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
54		fnfvof	⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
55	46 47 48 24 54	syl22anc	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
56	55	oveq2d	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
57	45 53 56	3eqtr4d	⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) )
58	2 3 4 5 6 7 9 11 13 21 57	islmhmd	⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 LMHom 𝑁 ) )