lfladdcl

Description: Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	lfladdcl.r	$⊢ R = Scalar (W)$
	lfladdcl.p	$⊢ \underset{˙}{+} = +_{R}$
	lfladdcl.f	$⊢ F = LFnl (W)$
	lfladdcl.w	$⊢ φ \to W \in LMod$
	lfladdcl.g	$⊢ φ \to G \in F$
	lfladdcl.h	$⊢ φ \to H \in F$
Assertion	lfladdcl	$⊢ φ \to G {\underset{˙}{+}}_{f} H \in F$

Proof

Step	Hyp	Ref	Expression
1		lfladdcl.r	$⊢ R = Scalar (W)$
2		lfladdcl.p	$⊢ \underset{˙}{+} = +_{R}$
3		lfladdcl.f	$⊢ F = LFnl (W)$
4		lfladdcl.w	$⊢ φ \to W \in LMod$
5		lfladdcl.g	$⊢ φ \to G \in F$
6		lfladdcl.h	$⊢ φ \to H \in F$
7	4	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to W \in LMod$
8		simprl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \in {Base}_{R}$
9		simprr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to y \in {Base}_{R}$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	1 10 2	lmodacl	$⊢ (W \in LMod \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{+} y \in {Base}_{R}$
12	7 8 9 11	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \underset{˙}{+} y \in {Base}_{R}$
13		eqid	$⊢ {Base}_{W} = {Base}_{W}$
14	1 10 13 3	lflf	$⊢ (W \in LMod \land G \in F) \to G : {Base}_{W} ⟶ {Base}_{R}$
15	4 5 14	syl2anc	$⊢ φ \to G : {Base}_{W} ⟶ {Base}_{R}$
16	1 10 13 3	lflf	$⊢ (W \in LMod \land H \in F) \to H : {Base}_{W} ⟶ {Base}_{R}$
17	4 6 16	syl2anc	$⊢ φ \to H : {Base}_{W} ⟶ {Base}_{R}$
18		fvexd	$⊢ φ \to {Base}_{W} \in V$
19		inidm	$⊢ {Base}_{W} \cap {Base}_{W} = {Base}_{W}$
20	12 15 17 18 18 19	off	$⊢ φ \to (G {\underset{˙}{+}}_{f} H) : {Base}_{W} ⟶ {Base}_{R}$
21	4	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to W \in LMod$
22		simpr1	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \in {Base}_{R}$
23		simpr2	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to y \in {Base}_{W}$
24		eqid	$⊢ \cdot_{W} = \cdot_{W}$
25	13 1 24 10	lmodvscl	$⊢ (W \in LMod \land x \in {Base}_{R} \land y \in {Base}_{W}) \to x \cdot_{W} y \in {Base}_{W}$
26	21 22 23 25	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{W} y \in {Base}_{W}$
27		simpr3	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to z \in {Base}_{W}$
28		eqid	$⊢ +_{W} = +_{W}$
29	13 28	lmodvacl	$⊢ (W \in LMod \land x \cdot_{W} y \in {Base}_{W} \land z \in {Base}_{W}) \to (x \cdot_{W} y) +_{W} z \in {Base}_{W}$
30	21 26 27 29	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{W} y) +_{W} z \in {Base}_{W}$
31	15	ffnd	$⊢ φ \to G Fn {Base}_{W}$
32	17	ffnd	$⊢ φ \to H Fn {Base}_{W}$
33		eqidd	$⊢ (φ \land (x \cdot_{W} y) +_{W} z \in {Base}_{W}) \to G ((x \cdot_{W} y) +_{W} z) = G ((x \cdot_{W} y) +_{W} z)$
34		eqidd	$⊢ (φ \land (x \cdot_{W} y) +_{W} z \in {Base}_{W}) \to H ((x \cdot_{W} y) +_{W} z) = H ((x \cdot_{W} y) +_{W} z)$
35	31 32 18 18 19 33 34	ofval	$⊢ (φ \land (x \cdot_{W} y) +_{W} z \in {Base}_{W}) \to (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = G ((x \cdot_{W} y) +_{W} z) \underset{˙}{+} H ((x \cdot_{W} y) +_{W} z)$
36	30 35	syldan	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = G ((x \cdot_{W} y) +_{W} z) \underset{˙}{+} H ((x \cdot_{W} y) +_{W} z)$
37		eqidd	$⊢ (φ \land y \in {Base}_{W}) \to G (y) = G (y)$
38		eqidd	$⊢ (φ \land y \in {Base}_{W}) \to H (y) = H (y)$
39	31 32 18 18 19 37 38	ofval	$⊢ (φ \land y \in {Base}_{W}) \to (G {\underset{˙}{+}}_{f} H) (y) = G (y) \underset{˙}{+} H (y)$
40	23 39	syldan	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G {\underset{˙}{+}}_{f} H) (y) = G (y) \underset{˙}{+} H (y)$
41	40	oveq2d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y) = x \cdot_{R} (G (y) \underset{˙}{+} H (y))$
42		eqidd	$⊢ (φ \land z \in {Base}_{W}) \to G (z) = G (z)$
43		eqidd	$⊢ (φ \land z \in {Base}_{W}) \to H (z) = H (z)$
44	31 32 18 18 19 42 43	ofval	$⊢ (φ \land z \in {Base}_{W}) \to (G {\underset{˙}{+}}_{f} H) (z) = G (z) \underset{˙}{+} H (z)$
45	27 44	syldan	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G {\underset{˙}{+}}_{f} H) (z) = G (z) \underset{˙}{+} H (z)$
46	41 45	oveq12d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z) = (x \cdot_{R} (G (y) \underset{˙}{+} H (y))) \underset{˙}{+} (G (z) \underset{˙}{+} H (z))$
47	5	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G \in F$
48	1 2 13 28 3	lfladd	$⊢ (W \in LMod \land G \in F \land (x \cdot_{W} y \in {Base}_{W} \land z \in {Base}_{W})) \to G ((x \cdot_{W} y) +_{W} z) = G (x \cdot_{W} y) \underset{˙}{+} G (z)$
49	21 47 26 27 48	syl112anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G ((x \cdot_{W} y) +_{W} z) = G (x \cdot_{W} y) \underset{˙}{+} G (z)$
50	6	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H \in F$
51	1 2 13 28 3	lfladd	$⊢ (W \in LMod \land H \in F \land (x \cdot_{W} y \in {Base}_{W} \land z \in {Base}_{W})) \to H ((x \cdot_{W} y) +_{W} z) = H (x \cdot_{W} y) \underset{˙}{+} H (z)$
52	21 50 26 27 51	syl112anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H ((x \cdot_{W} y) +_{W} z) = H (x \cdot_{W} y) \underset{˙}{+} H (z)$
53	49 52	oveq12d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G ((x \cdot_{W} y) +_{W} z) \underset{˙}{+} H ((x \cdot_{W} y) +_{W} z) = (G (x \cdot_{W} y) \underset{˙}{+} G (z)) \underset{˙}{+} (H (x \cdot_{W} y) \underset{˙}{+} H (z))$
54	1	lmodring	$⊢ W \in LMod \to R \in Ring$
55	21 54	syl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to R \in Ring$
56		ringcmn	$⊢ R \in Ring \to R \in CMnd$
57	55 56	syl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to R \in CMnd$
58	1 10 13 3	lflcl	$⊢ (W \in LMod \land G \in F \land x \cdot_{W} y \in {Base}_{W}) \to G (x \cdot_{W} y) \in {Base}_{R}$
59	21 47 26 58	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (x \cdot_{W} y) \in {Base}_{R}$
60	1 10 13 3	lflcl	$⊢ (W \in LMod \land G \in F \land z \in {Base}_{W}) \to G (z) \in {Base}_{R}$
61	21 47 27 60	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (z) \in {Base}_{R}$
62	1 10 13 3	lflcl	$⊢ (W \in LMod \land H \in F \land x \cdot_{W} y \in {Base}_{W}) \to H (x \cdot_{W} y) \in {Base}_{R}$
63	21 50 26 62	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H (x \cdot_{W} y) \in {Base}_{R}$
64	1 10 13 3	lflcl	$⊢ (W \in LMod \land H \in F \land z \in {Base}_{W}) \to H (z) \in {Base}_{R}$
65	21 50 27 64	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H (z) \in {Base}_{R}$
66	10 2	cmn4	$⊢ (R \in CMnd \land (G (x \cdot_{W} y) \in {Base}_{R} \land G (z) \in {Base}_{R}) \land (H (x \cdot_{W} y) \in {Base}_{R} \land H (z) \in {Base}_{R})) \to (G (x \cdot_{W} y) \underset{˙}{+} G (z)) \underset{˙}{+} (H (x \cdot_{W} y) \underset{˙}{+} H (z)) = (G (x \cdot_{W} y) \underset{˙}{+} H (x \cdot_{W} y)) \underset{˙}{+} (G (z) \underset{˙}{+} H (z))$
67	57 59 61 63 65 66	syl122anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G (x \cdot_{W} y) \underset{˙}{+} G (z)) \underset{˙}{+} (H (x \cdot_{W} y) \underset{˙}{+} H (z)) = (G (x \cdot_{W} y) \underset{˙}{+} H (x \cdot_{W} y)) \underset{˙}{+} (G (z) \underset{˙}{+} H (z))$
68		eqid	$⊢ \cdot_{R} = \cdot_{R}$
69	1 10 68 13 24 3	lflmul	$⊢ (W \in LMod \land G \in F \land (x \in {Base}_{R} \land y \in {Base}_{W})) \to G (x \cdot_{W} y) = x \cdot_{R} G (y)$
70	21 47 22 23 69	syl112anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (x \cdot_{W} y) = x \cdot_{R} G (y)$
71	1 10 68 13 24 3	lflmul	$⊢ (W \in LMod \land H \in F \land (x \in {Base}_{R} \land y \in {Base}_{W})) \to H (x \cdot_{W} y) = x \cdot_{R} H (y)$
72	21 50 22 23 71	syl112anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H (x \cdot_{W} y) = x \cdot_{R} H (y)$
73	70 72	oveq12d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (x \cdot_{W} y) \underset{˙}{+} H (x \cdot_{W} y) = (x \cdot_{R} G (y)) \underset{˙}{+} (x \cdot_{R} H (y))$
74	1 10 13 3	lflcl	$⊢ (W \in LMod \land G \in F \land y \in {Base}_{W}) \to G (y) \in {Base}_{R}$
75	21 47 23 74	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (y) \in {Base}_{R}$
76	1 10 13 3	lflcl	$⊢ (W \in LMod \land H \in F \land y \in {Base}_{W}) \to H (y) \in {Base}_{R}$
77	21 50 23 76	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to H (y) \in {Base}_{R}$
78	10 2 68	ringdi	$⊢ (R \in Ring \land (x \in {Base}_{R} \land G (y) \in {Base}_{R} \land H (y) \in {Base}_{R})) \to x \cdot_{R} (G (y) \underset{˙}{+} H (y)) = (x \cdot_{R} G (y)) \underset{˙}{+} (x \cdot_{R} H (y))$
79	55 22 75 77 78	syl13anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{R} (G (y) \underset{˙}{+} H (y)) = (x \cdot_{R} G (y)) \underset{˙}{+} (x \cdot_{R} H (y))$
80	73 79	eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G (x \cdot_{W} y) \underset{˙}{+} H (x \cdot_{W} y) = x \cdot_{R} (G (y) \underset{˙}{+} H (y))$
81	80	oveq1d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G (x \cdot_{W} y) \underset{˙}{+} H (x \cdot_{W} y)) \underset{˙}{+} (G (z) \underset{˙}{+} H (z)) = (x \cdot_{R} (G (y) \underset{˙}{+} H (y))) \underset{˙}{+} (G (z) \underset{˙}{+} H (z))$
82	53 67 81	3eqtrd	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to G ((x \cdot_{W} y) +_{W} z) \underset{˙}{+} H ((x \cdot_{W} y) +_{W} z) = (x \cdot_{R} (G (y) \underset{˙}{+} H (y))) \underset{˙}{+} (G (z) \underset{˙}{+} H (z))$
83	46 82	eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z) = G ((x \cdot_{W} y) +_{W} z) \underset{˙}{+} H ((x \cdot_{W} y) +_{W} z)$
84	36 83	eqtr4d	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z)$
85	84	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{R} \forall y \in {Base}_{W} \forall z \in {Base}_{W} (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z)$
86	13 28 1 24 10 2 68 3	islfl	$⊢ W \in LMod \to (G {\underset{˙}{+}}_{f} H \in F \leftrightarrow ((G {\underset{˙}{+}}_{f} H) : {Base}_{W} ⟶ {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{W} \forall z \in {Base}_{W} (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z)))$
87	4 86	syl	$⊢ φ \to (G {\underset{˙}{+}}_{f} H \in F \leftrightarrow ((G {\underset{˙}{+}}_{f} H) : {Base}_{W} ⟶ {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{W} \forall z \in {Base}_{W} (G {\underset{˙}{+}}_{f} H) ((x \cdot_{W} y) +_{W} z) = (x \cdot_{R} (G {\underset{˙}{+}}_{f} H) (y)) \underset{˙}{+} (G {\underset{˙}{+}}_{f} H) (z)))$
88	20 85 87	mpbir2and	$⊢ φ \to G {\underset{˙}{+}}_{f} H \in F$

Metamath Proof Explorer

Theorem lfladdcl

Proof