ghmplusg

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

		Ref	Expression
	Hypothesis	ghmplusg.p	$⊢ \underset{˙}{+} = +_{N}$
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		ghmplusg.p	$⊢ \underset{˙}{+} = +_{N}$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ {Base}_{N} = {Base}_{N}$
4		eqid	$⊢ +_{M} = +_{M}$
5		ghmgrp1	$⊢ G \in (M GrpHom N) \to M \in Grp$
6	5	3ad2ant3	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to M \in Grp$
7		ghmgrp2	$⊢ G \in (M GrpHom N) \to N \in Grp$
8	7	3ad2ant3	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to N \in Grp$
9	3 1	grpcl	$⊢ (N \in Grp \land x \in {Base}_{N} \land y \in {Base}_{N}) \to x \underset{˙}{+} y \in {Base}_{N}$
10	9	3expb	$⊢ (N \in Grp \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to x \underset{˙}{+} y \in {Base}_{N}$
11	8 10	sylan	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to x \underset{˙}{+} y \in {Base}_{N}$
12	2 3	ghmf	$⊢ F \in (M GrpHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
13	12	3ad2ant2	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to F : {Base}_{M} ⟶ {Base}_{N}$
14	2 3	ghmf	$⊢ G \in (M GrpHom N) \to G : {Base}_{M} ⟶ {Base}_{N}$
15	14	3ad2ant3	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to G : {Base}_{M} ⟶ {Base}_{N}$
16		fvexd	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to {Base}_{M} \in V$
17		inidm	$⊢ {Base}_{M} \cap {Base}_{M} = {Base}_{M}$
18	11 13 15 16 16 17	off	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to (F {\underset{˙}{+}}_{f} G) : {Base}_{M} ⟶ {Base}_{N}$
19	2 4 1	ghmlin	$⊢ (F \in (M GrpHom N) \land x \in {Base}_{M} \land y \in {Base}_{M}) \to F (x +_{M} y) = F (x) \underset{˙}{+} F (y)$
20	19	3expb	$⊢ (F \in (M GrpHom N) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (x +_{M} y) = F (x) \underset{˙}{+} F (y)$
21	20	3ad2antl2	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (x +_{M} y) = F (x) \underset{˙}{+} F (y)$
22	2 4 1	ghmlin	$⊢ (G \in (M GrpHom N) \land x \in {Base}_{M} \land y \in {Base}_{M}) \to G (x +_{M} y) = G (x) \underset{˙}{+} G (y)$
23	22	3expb	$⊢ (G \in (M GrpHom N) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to G (x +_{M} y) = G (x) \underset{˙}{+} G (y)$
24	23	3ad2antl3	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to G (x +_{M} y) = G (x) \underset{˙}{+} G (y)$
25	21 24	oveq12d	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (x +_{M} y) \underset{˙}{+} G (x +_{M} y) = (F (x) \underset{˙}{+} F (y)) \underset{˙}{+} (G (x) \underset{˙}{+} G (y))$
26		simpl1	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to N \in Abel$
27		ablcmn	$⊢ N \in Abel \to N \in CMnd$
28	26 27	syl	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to N \in CMnd$
29	13	ffvelcdmda	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land x \in {Base}_{M}) \to F (x) \in {Base}_{N}$
30	29	adantrr	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (x) \in {Base}_{N}$
31	13	ffvelcdmda	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land y \in {Base}_{M}) \to F (y) \in {Base}_{N}$
32	31	adantrl	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (y) \in {Base}_{N}$
33	15	ffvelcdmda	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land x \in {Base}_{M}) \to G (x) \in {Base}_{N}$
34	33	adantrr	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to G (x) \in {Base}_{N}$
35	15	ffvelcdmda	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land y \in {Base}_{M}) \to G (y) \in {Base}_{N}$
36	35	adantrl	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to G (y) \in {Base}_{N}$
37	3 1	cmn4	$⊢ (N \in CMnd \land (F (x) \in {Base}_{N} \land F (y) \in {Base}_{N}) \land (G (x) \in {Base}_{N} \land G (y) \in {Base}_{N})) \to (F (x) \underset{˙}{+} F (y)) \underset{˙}{+} (G (x) \underset{˙}{+} G (y)) = (F (x) \underset{˙}{+} G (x)) \underset{˙}{+} (F (y) \underset{˙}{+} G (y))$
38	28 30 32 34 36 37	syl122anc	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F (x) \underset{˙}{+} F (y)) \underset{˙}{+} (G (x) \underset{˙}{+} G (y)) = (F (x) \underset{˙}{+} G (x)) \underset{˙}{+} (F (y) \underset{˙}{+} G (y))$
39	25 38	eqtrd	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F (x +_{M} y) \underset{˙}{+} G (x +_{M} y) = (F (x) \underset{˙}{+} G (x)) \underset{˙}{+} (F (y) \underset{˙}{+} G (y))$
40	13	ffnd	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to F Fn {Base}_{M}$
41	40	adantr	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to F Fn {Base}_{M}$
42	15	ffnd	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to G Fn {Base}_{M}$
43	42	adantr	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to G Fn {Base}_{M}$
44		fvexd	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to {Base}_{M} \in V$
45	2 4	grpcl	$⊢ (M \in Grp \land x \in {Base}_{M} \land y \in {Base}_{M}) \to x +_{M} y \in {Base}_{M}$
46	45	3expb	$⊢ (M \in Grp \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to x +_{M} y \in {Base}_{M}$
47	6 46	sylan	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to x +_{M} y \in {Base}_{M}$
48		fnfvof	$⊢ ((F Fn {Base}_{M} \land G Fn {Base}_{M}) \land ({Base}_{M} \in V \land x +_{M} y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x +_{M} y) = F (x +_{M} y) \underset{˙}{+} G (x +_{M} y)$
49	41 43 44 47 48	syl22anc	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x +_{M} y) = F (x +_{M} y) \underset{˙}{+} G (x +_{M} y)$
50		simprl	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to x \in {Base}_{M}$
51		fnfvof	$⊢ ((F Fn {Base}_{M} \land G Fn {Base}_{M}) \land ({Base}_{M} \in V \land x \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x) = F (x) \underset{˙}{+} G (x)$
52	41 43 44 50 51	syl22anc	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x) = F (x) \underset{˙}{+} G (x)$
53		simprr	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to y \in {Base}_{M}$
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	41 43 44 53 54	syl22anc	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (y) = F (y) \underset{˙}{+} G (y)$
56	52 55	oveq12d	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x) \underset{˙}{+} (F {\underset{˙}{+}}_{f} G) (y) = (F (x) \underset{˙}{+} G (x)) \underset{˙}{+} (F (y) \underset{˙}{+} G (y))$
57	39 49 56	3eqtr4d	$⊢ ((N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \land (x \in {Base}_{M} \land y \in {Base}_{M})) \to (F {\underset{˙}{+}}_{f} G) (x +_{M} y) = (F {\underset{˙}{+}}_{f} G) (x) \underset{˙}{+} (F {\underset{˙}{+}}_{f} G) (y)$
58	2 3 4 1 6 8 18 57	isghmd	$⊢ (N \in Abel \land F \in (M GrpHom N) \land G \in (M GrpHom N)) \to F {\underset{˙}{+}}_{f} G \in (M GrpHom N)$

Metamath Proof Explorer

Theorem ghmplusg

Proof