hgmapadd

	Ref	Expression
Hypotheses	hgmapadd.h	$⊢ H = LHyp (K)$
	hgmapadd.u	$⊢ U = DVecH (K) (W)$
	hgmapadd.r	$⊢ R = Scalar (U)$
	hgmapadd.b	$⊢ B = {Base}_{R}$
	hgmapadd.p	$⊢ \underset{˙}{+} = +_{R}$
	hgmapadd.g	$⊢ G = HGMap (K) (W)$
	hgmapadd.k	$⊢ φ \to (K \in HL \land W \in H)$
	hgmapadd.x	$⊢ φ \to X \in B$
	hgmapadd.y	$⊢ φ \to Y \in B$
Assertion	hgmapadd	$⊢ φ \to G (X \underset{˙}{+} Y) = G (X) \underset{˙}{+} G (Y)$

Proof

Step	Hyp	Ref	Expression
1		hgmapadd.h	$⊢ H = LHyp (K)$
2		hgmapadd.u	$⊢ U = DVecH (K) (W)$
3		hgmapadd.r	$⊢ R = Scalar (U)$
4		hgmapadd.b	$⊢ B = {Base}_{R}$
5		hgmapadd.p	$⊢ \underset{˙}{+} = +_{R}$
6		hgmapadd.g	$⊢ G = HGMap (K) (W)$
7		hgmapadd.k	$⊢ φ \to (K \in HL \land W \in H)$
8		hgmapadd.x	$⊢ φ \to X \in B$
9		hgmapadd.y	$⊢ φ \to Y \in B$
10		eqid	$⊢ {Base}_{U} = {Base}_{U}$
11		eqid	$⊢ 0_{U} = 0_{U}$
12	1 2 10 11 7	dvh1dim	$⊢ φ \to \exists t \in {Base}_{U} t \neq 0_{U}$
13		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
14	1 13 7	lcdlmod	$⊢ φ \to LCDual (K) (W) \in LMod$
15	14	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to LCDual (K) (W) \in LMod$
16		eqid	$⊢ Scalar (LCDual (K) (W)) = Scalar (LCDual (K) (W))$
17		eqid	$⊢ {Base}_{Scalar (LCDual (K) (W))} = {Base}_{Scalar (LCDual (K) (W))}$
18	7	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (K \in HL \land W \in H)$
19	8	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \in B$
20	1 2 3 4 13 16 17 6 18 19	hgmapdcl	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X) \in {Base}_{Scalar (LCDual (K) (W))}$
21	1 2 3 4 13 16 17 6 7 9	hgmapdcl	$⊢ φ \to G (Y) \in {Base}_{Scalar (LCDual (K) (W))}$
22	21	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (Y) \in {Base}_{Scalar (LCDual (K) (W))}$
23		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
24		eqid	$⊢ HDMap (K) (W) = HDMap (K) (W)$
25		simp2	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to t \in {Base}_{U}$
26	1 2 10 13 23 24 18 25	hdmapcl	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (t) \in {Base}_{LCDual (K) (W)}$
27		eqid	$⊢ +_{LCDual (K) (W)} = +_{LCDual (K) (W)}$
28		eqid	$⊢ \cdot_{LCDual (K) (W)} = \cdot_{LCDual (K) (W)}$
29		eqid	$⊢ +_{Scalar (LCDual (K) (W))} = +_{Scalar (LCDual (K) (W))}$
30	23 27 16 28 17 29	lmodvsdir	$⊢ (LCDual (K) (W) \in LMod \land (G (X) \in {Base}_{Scalar (LCDual (K) (W))} \land G (Y) \in {Base}_{Scalar (LCDual (K) (W))} \land HDMap (K) (W) (t) \in {Base}_{LCDual (K) (W)})) \to (G (X) +_{Scalar (LCDual (K) (W))} G (Y)) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) = (G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)) +_{LCDual (K) (W)} (G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t))$
31	15 20 22 26 30	syl13anc	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (G (X) +_{Scalar (LCDual (K) (W))} G (Y)) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) = (G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)) +_{LCDual (K) (W)} (G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t))$
32	1 2 7	dvhlmod	$⊢ φ \to U \in LMod$
33	32	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to U \in LMod$
34	9	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to Y \in B$
35		eqid	$⊢ +_{U} = +_{U}$
36		eqid	$⊢ \cdot_{U} = \cdot_{U}$
37	10 35 3 36 4 5	lmodvsdir	$⊢ (U \in LMod \land (X \in B \land Y \in B \land t \in {Base}_{U})) \to (X \underset{˙}{+} Y) \cdot_{U} t = (X \cdot_{U} t) +_{U} (Y \cdot_{U} t)$
38	33 19 34 25 37	syl13anc	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (X \underset{˙}{+} Y) \cdot_{U} t = (X \cdot_{U} t) +_{U} (Y \cdot_{U} t)$
39	38	fveq2d	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) ((X \underset{˙}{+} Y) \cdot_{U} t) = HDMap (K) (W) ((X \cdot_{U} t) +_{U} (Y \cdot_{U} t))$
40	10 3 36 4	lmodvscl	$⊢ (U \in LMod \land X \in B \land t \in {Base}_{U}) \to X \cdot_{U} t \in {Base}_{U}$
41	33 19 25 40	syl3anc	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \cdot_{U} t \in {Base}_{U}$
42	10 3 36 4	lmodvscl	$⊢ (U \in LMod \land Y \in B \land t \in {Base}_{U}) \to Y \cdot_{U} t \in {Base}_{U}$
43	33 34 25 42	syl3anc	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to Y \cdot_{U} t \in {Base}_{U}$
44	1 2 10 35 13 27 24 18 41 43	hdmapadd	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) ((X \cdot_{U} t) +_{U} (Y \cdot_{U} t)) = HDMap (K) (W) (X \cdot_{U} t) +_{LCDual (K) (W)} HDMap (K) (W) (Y \cdot_{U} t)$
45	1 2 10 36 3 4 13 28 24 6 18 25 19	hgmapvs	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (X \cdot_{U} t) = G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
46	1 2 10 36 3 4 13 28 24 6 18 25 34	hgmapvs	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (Y \cdot_{U} t) = G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
47	45 46	oveq12d	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (X \cdot_{U} t) +_{LCDual (K) (W)} HDMap (K) (W) (Y \cdot_{U} t) = (G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)) +_{LCDual (K) (W)} (G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t))$
48	39 44 47	3eqtrrd	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (G (X) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)) +_{LCDual (K) (W)} (G (Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)) = HDMap (K) (W) ((X \underset{˙}{+} Y) \cdot_{U} t)$
49	3 4 5	lmodacl	$⊢ (U \in LMod \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
50	32 8 9 49	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in B$
51	50	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to X \underset{˙}{+} Y \in B$
52	1 2 10 36 3 4 13 28 24 6 18 25 51	hgmapvs	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) ((X \underset{˙}{+} Y) \cdot_{U} t) = G (X \underset{˙}{+} Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
53	31 48 52	3eqtrrd	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X \underset{˙}{+} Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) = (G (X) +_{Scalar (LCDual (K) (W))} G (Y)) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t)$
54		eqid	$⊢ 0_{LCDual (K) (W)} = 0_{LCDual (K) (W)}$
55	1 13 7	lcdlvec	$⊢ φ \to LCDual (K) (W) \in LVec$
56	55	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to LCDual (K) (W) \in LVec$
57	1 2 3 4 13 16 17 6 7 50	hgmapdcl	$⊢ φ \to G (X \underset{˙}{+} Y) \in {Base}_{Scalar (LCDual (K) (W))}$
58	57	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X \underset{˙}{+} Y) \in {Base}_{Scalar (LCDual (K) (W))}$
59	1 2 3 4 13 16 17 6 7 8	hgmapdcl	$⊢ φ \to G (X) \in {Base}_{Scalar (LCDual (K) (W))}$
60	16 17 29	lmodacl	$⊢ (LCDual (K) (W) \in LMod \land G (X) \in {Base}_{Scalar (LCDual (K) (W))} \land G (Y) \in {Base}_{Scalar (LCDual (K) (W))}) \to G (X) +_{Scalar (LCDual (K) (W))} G (Y) \in {Base}_{Scalar (LCDual (K) (W))}$
61	14 59 21 60	syl3anc	$⊢ φ \to G (X) +_{Scalar (LCDual (K) (W))} G (Y) \in {Base}_{Scalar (LCDual (K) (W))}$
62	61	3ad2ant1	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X) +_{Scalar (LCDual (K) (W))} G (Y) \in {Base}_{Scalar (LCDual (K) (W))}$
63		simp3	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to t \neq 0_{U}$
64	1 2 10 11 13 54 24 18 25	hdmapeq0	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (HDMap (K) (W) (t) = 0_{LCDual (K) (W)} \leftrightarrow t = 0_{U})$
65	64	necon3bid	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (HDMap (K) (W) (t) \neq 0_{LCDual (K) (W)} \leftrightarrow t \neq 0_{U})$
66	63 65	mpbird	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to HDMap (K) (W) (t) \neq 0_{LCDual (K) (W)}$
67	23 28 16 17 54 56 58 62 26 66	lvecvscan2	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to (G (X \underset{˙}{+} Y) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) = (G (X) +_{Scalar (LCDual (K) (W))} G (Y)) \cdot_{LCDual (K) (W)} HDMap (K) (W) (t) \leftrightarrow G (X \underset{˙}{+} Y) = G (X) +_{Scalar (LCDual (K) (W))} G (Y))$
68	53 67	mpbid	$⊢ (φ \land t \in {Base}_{U} \land t \neq 0_{U}) \to G (X \underset{˙}{+} Y) = G (X) +_{Scalar (LCDual (K) (W))} G (Y)$
69	68	rexlimdv3a	$⊢ φ \to (\exists t \in {Base}_{U} t \neq 0_{U} \to G (X \underset{˙}{+} Y) = G (X) +_{Scalar (LCDual (K) (W))} G (Y))$
70	12 69	mpd	$⊢ φ \to G (X \underset{˙}{+} Y) = G (X) +_{Scalar (LCDual (K) (W))} G (Y)$
71	1 2 3 5 13 16 29 7	lcdsadd	$⊢ φ \to +_{Scalar (LCDual (K) (W))} = \underset{˙}{+}$
72	71	oveqd	$⊢ φ \to G (X) +_{Scalar (LCDual (K) (W))} G (Y) = G (X) \underset{˙}{+} G (Y)$
73	70 72	eqtrd	$⊢ φ \to G (X \underset{˙}{+} Y) = G (X) \underset{˙}{+} G (Y)$

Metamath Proof Explorer

Theorem hgmapadd

Proof