hdmap14lem8

Description: Part of proof of part 14 in Baer p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem8.h	$⊢ H = LHyp (K)$
	hdmap14lem8.u	$⊢ U = DVecH (K) (W)$
	hdmap14lem8.v	$⊢ V = {Base}_{U}$
	hdmap14lem8.q	$⊢ \underset{˙}{+} = +_{U}$
	hdmap14lem8.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmap14lem8.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap14lem8.n	$⊢ N = LSpan (U)$
	hdmap14lem8.r	$⊢ R = Scalar (U)$
	hdmap14lem8.b	$⊢ B = {Base}_{R}$
	hdmap14lem8.c	$⊢ C = LCDual (K) (W)$
	hdmap14lem8.d	$⊢ \underset{˙}{✚} = +_{C}$
	hdmap14lem8.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
	hdmap14lem8.p	$⊢ P = Scalar (C)$
	hdmap14lem8.a	$⊢ A = {Base}_{P}$
	hdmap14lem8.s	$⊢ S = HDMap (K) (W)$
	hdmap14lem8.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap14lem8.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap14lem8.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap14lem8.f	$⊢ φ \to F \in B$
	hdmap14lem8.g	$⊢ φ \to G \in A$
	hdmap14lem8.i	$⊢ φ \to I \in A$
	hdmap14lem8.xx	$⊢ φ \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
	hdmap14lem8.yy	$⊢ φ \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
	hdmap14lem8.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	hdmap14lem8.j	$⊢ φ \to J \in A$
	hdmap14lem8.xy	$⊢ φ \to S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = J \underset{˙}{∙} S (X \underset{˙}{+} Y)$
Assertion	hdmap14lem8	$⊢ φ \to (J \underset{˙}{∙} S (X)) \underset{˙}{✚} (J \underset{˙}{∙} S (Y)) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem8.h	$⊢ H = LHyp (K)$
2		hdmap14lem8.u	$⊢ U = DVecH (K) (W)$
3		hdmap14lem8.v	$⊢ V = {Base}_{U}$
4		hdmap14lem8.q	$⊢ \underset{˙}{+} = +_{U}$
5		hdmap14lem8.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
6		hdmap14lem8.o	$⊢ \underset{˙}{0} = 0_{U}$
7		hdmap14lem8.n	$⊢ N = LSpan (U)$
8		hdmap14lem8.r	$⊢ R = Scalar (U)$
9		hdmap14lem8.b	$⊢ B = {Base}_{R}$
10		hdmap14lem8.c	$⊢ C = LCDual (K) (W)$
11		hdmap14lem8.d	$⊢ \underset{˙}{✚} = +_{C}$
12		hdmap14lem8.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
13		hdmap14lem8.p	$⊢ P = Scalar (C)$
14		hdmap14lem8.a	$⊢ A = {Base}_{P}$
15		hdmap14lem8.s	$⊢ S = HDMap (K) (W)$
16		hdmap14lem8.k	$⊢ φ \to (K \in HL \land W \in H)$
17		hdmap14lem8.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		hdmap14lem8.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
19		hdmap14lem8.f	$⊢ φ \to F \in B$
20		hdmap14lem8.g	$⊢ φ \to G \in A$
21		hdmap14lem8.i	$⊢ φ \to I \in A$
22		hdmap14lem8.xx	$⊢ φ \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
23		hdmap14lem8.yy	$⊢ φ \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
24		hdmap14lem8.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
25		hdmap14lem8.j	$⊢ φ \to J \in A$
26		hdmap14lem8.xy	$⊢ φ \to S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = J \underset{˙}{∙} S (X \underset{˙}{+} Y)$
27	1 10 16	lcdlmod	$⊢ φ \to C \in LMod$
28		eqid	$⊢ {Base}_{C} = {Base}_{C}$
29	17	eldifad	$⊢ φ \to X \in V$
30	1 2 3 10 28 15 16 29	hdmapcl	$⊢ φ \to S (X) \in {Base}_{C}$
31	18	eldifad	$⊢ φ \to Y \in V$
32	1 2 3 10 28 15 16 31	hdmapcl	$⊢ φ \to S (Y) \in {Base}_{C}$
33	28 11 13 12 14	lmodvsdi	$⊢ (C \in LMod \land (J \in A \land S (X) \in {Base}_{C} \land S (Y) \in {Base}_{C})) \to J \underset{˙}{∙} (S (X) \underset{˙}{✚} S (Y)) = (J \underset{˙}{∙} S (X)) \underset{˙}{✚} (J \underset{˙}{∙} S (Y))$
34	27 25 30 32 33	syl13anc	$⊢ φ \to J \underset{˙}{∙} (S (X) \underset{˙}{✚} S (Y)) = (J \underset{˙}{∙} S (X)) \underset{˙}{✚} (J \underset{˙}{∙} S (Y))$
35	1 2 3 4 10 11 15 16 29 31	hdmapadd	$⊢ φ \to S (X \underset{˙}{+} Y) = S (X) \underset{˙}{✚} S (Y)$
36	35	oveq2d	$⊢ φ \to J \underset{˙}{∙} S (X \underset{˙}{+} Y) = J \underset{˙}{∙} (S (X) \underset{˙}{✚} S (Y))$
37	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
38	3 4 8 5 9	lmodvsdi	$⊢ (U \in LMod \land (F \in B \land X \in V \land Y \in V)) \to F \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (F \underset{˙}{\cdot} X) \underset{˙}{+} (F \underset{˙}{\cdot} Y)$
39	37 19 29 31 38	syl13anc	$⊢ φ \to F \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (F \underset{˙}{\cdot} X) \underset{˙}{+} (F \underset{˙}{\cdot} Y)$
40	39	fveq2d	$⊢ φ \to S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = S ((F \underset{˙}{\cdot} X) \underset{˙}{+} (F \underset{˙}{\cdot} Y))$
41	3 8 5 9	lmodvscl	$⊢ (U \in LMod \land F \in B \land X \in V) \to F \underset{˙}{\cdot} X \in V$
42	37 19 29 41	syl3anc	$⊢ φ \to F \underset{˙}{\cdot} X \in V$
43	3 8 5 9	lmodvscl	$⊢ (U \in LMod \land F \in B \land Y \in V) \to F \underset{˙}{\cdot} Y \in V$
44	37 19 31 43	syl3anc	$⊢ φ \to F \underset{˙}{\cdot} Y \in V$
45	1 2 3 4 10 11 15 16 42 44	hdmapadd	$⊢ φ \to S ((F \underset{˙}{\cdot} X) \underset{˙}{+} (F \underset{˙}{\cdot} Y)) = S (F \underset{˙}{\cdot} X) \underset{˙}{✚} S (F \underset{˙}{\cdot} Y)$
46	22 23	oveq12d	$⊢ φ \to S (F \underset{˙}{\cdot} X) \underset{˙}{✚} S (F \underset{˙}{\cdot} Y) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$
47	40 45 46	3eqtrd	$⊢ φ \to S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$
48	26 47	eqtr3d	$⊢ φ \to J \underset{˙}{∙} S (X \underset{˙}{+} Y) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$
49	36 48	eqtr3d	$⊢ φ \to J \underset{˙}{∙} (S (X) \underset{˙}{✚} S (Y)) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$
50	34 49	eqtr3d	$⊢ φ \to (J \underset{˙}{∙} S (X)) \underset{˙}{✚} (J \underset{˙}{∙} S (Y)) = (G \underset{˙}{∙} S (X)) \underset{˙}{✚} (I \underset{˙}{∙} S (Y))$

Metamath Proof Explorer

Theorem hdmap14lem8

Proof