hgmapmul

Description: Part 15 of Baer p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015)

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

Proof

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

Metamath Proof Explorer

Theorem hgmapmul

Proof