hdmapglem7a

	Ref	Expression
Hypotheses	hdmapglem7.h	$⊢ H = LHyp (K)$
	hdmapglem7.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapglem7.o	$⊢ O = ocH (K) (W)$
	hdmapglem7.u	$⊢ U = DVecH (K) (W)$
	hdmapglem7.v	$⊢ V = {Base}_{U}$
	hdmapglem7.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmapglem7.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmapglem7.r	$⊢ R = Scalar (U)$
	hdmapglem7.b	$⊢ B = {Base}_{R}$
	hdmapglem7.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	hdmapglem7.n	$⊢ N = LSpan (U)$
	hdmapglem7.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapglem7.x	$⊢ φ \to X \in V$
Assertion	hdmapglem7a	$⊢ φ \to \exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem7.h	$⊢ H = LHyp (K)$
2		hdmapglem7.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapglem7.o	$⊢ O = ocH (K) (W)$
4		hdmapglem7.u	$⊢ U = DVecH (K) (W)$
5		hdmapglem7.v	$⊢ V = {Base}_{U}$
6		hdmapglem7.p	$⊢ \underset{˙}{+} = +_{U}$
7		hdmapglem7.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
8		hdmapglem7.r	$⊢ R = Scalar (U)$
9		hdmapglem7.b	$⊢ B = {Base}_{R}$
10		hdmapglem7.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
11		hdmapglem7.n	$⊢ N = LSpan (U)$
12		hdmapglem7.k	$⊢ φ \to (K \in HL \land W \in H)$
13		hdmapglem7.x	$⊢ φ \to X \in V$
14		eqid	$⊢ LSubSp (U) = LSubSp (U)$
15	1 4 12	dvhlmod	$⊢ φ \to U \in LMod$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
18		eqid	$⊢ 0_{U} = 0_{U}$
19	1 16 17 4 5 18 2 12	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
20	19	eldifad	$⊢ φ \to E \in V$
21	5 14 11	lspsncl	$⊢ (U \in LMod \land E \in V) \to N (\{E\}) \in LSubSp (U)$
22	15 20 21	syl2anc	$⊢ φ \to N (\{E\}) \in LSubSp (U)$
23	20	snssd	$⊢ φ \to \{E\} \subseteq V$
24	1 4 3 5 11 12 23	dochocsp	$⊢ φ \to O (N (\{E\})) = O (\{E\})$
25	24	fveq2d	$⊢ φ \to O (O (N (\{E\}))) = O (O (\{E\}))$
26	1 4 3 5 11 12 20	dochocsn	$⊢ φ \to O (O (\{E\})) = N (\{E\})$
27	25 26	eqtrd	$⊢ φ \to O (O (N (\{E\}))) = N (\{E\})$
28	1 3 4 5 14 10 12 22 27	dochexmid	$⊢ φ \to N (\{E\}) \underset{˙}{\oplus} O (N (\{E\})) = V$
29	24	oveq2d	$⊢ φ \to N (\{E\}) \underset{˙}{\oplus} O (N (\{E\})) = N (\{E\}) \underset{˙}{\oplus} O (\{E\})$
30	28 29	eqtr3d	$⊢ φ \to V = N (\{E\}) \underset{˙}{\oplus} O (\{E\})$
31	13 30	eleqtrd	$⊢ φ \to X \in (N (\{E\}) \underset{˙}{\oplus} O (\{E\}))$
32	14	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
33	15 32	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
34	33 22	sseldd	$⊢ φ \to N (\{E\}) \in SubGrp (U)$
35	1 4 5 14 3	dochlss	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \in LSubSp (U)$
36	12 23 35	syl2anc	$⊢ φ \to O (\{E\}) \in LSubSp (U)$
37	33 36	sseldd	$⊢ φ \to O (\{E\}) \in SubGrp (U)$
38	6 10	lsmelval	$⊢ (N (\{E\}) \in SubGrp (U) \land O (\{E\}) \in SubGrp (U)) \to (X \in (N (\{E\}) \underset{˙}{\oplus} O (\{E\})) \leftrightarrow \exists a \in N (\{E\}) \exists u \in O (\{E\}) X = a \underset{˙}{+} u)$
39	34 37 38	syl2anc	$⊢ φ \to (X \in (N (\{E\}) \underset{˙}{\oplus} O (\{E\})) \leftrightarrow \exists a \in N (\{E\}) \exists u \in O (\{E\}) X = a \underset{˙}{+} u)$
40	31 39	mpbid	$⊢ φ \to \exists a \in N (\{E\}) \exists u \in O (\{E\}) X = a \underset{˙}{+} u$
41		rexcom	$⊢ \exists a \in N (\{E\}) \exists u \in O (\{E\}) X = a \underset{˙}{+} u \leftrightarrow \exists u \in O (\{E\}) \exists a \in N (\{E\}) X = a \underset{˙}{+} u$
42		df-rex	$⊢ \exists a \in N (\{E\}) X = a \underset{˙}{+} u \leftrightarrow \exists a (a \in N (\{E\}) \land X = a \underset{˙}{+} u)$
43	8 9 5 7 11	lspsnel	$⊢ (U \in LMod \land E \in V) \to (a \in N (\{E\}) \leftrightarrow \exists k \in B a = k \underset{˙}{\cdot} E)$
44	15 20 43	syl2anc	$⊢ φ \to (a \in N (\{E\}) \leftrightarrow \exists k \in B a = k \underset{˙}{\cdot} E)$
45	44	anbi1d	$⊢ φ \to ((a \in N (\{E\}) \land X = a \underset{˙}{+} u) \leftrightarrow (\exists k \in B a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u))$
46		r19.41v	$⊢ \exists k \in B (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u) \leftrightarrow (\exists k \in B a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u)$
47	45 46	bitr4di	$⊢ φ \to ((a \in N (\{E\}) \land X = a \underset{˙}{+} u) \leftrightarrow \exists k \in B (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u))$
48	47	exbidv	$⊢ φ \to (\exists a (a \in N (\{E\}) \land X = a \underset{˙}{+} u) \leftrightarrow \exists a \exists k \in B (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u))$
49		rexcom4	$⊢ \exists k \in B \exists a (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u) \leftrightarrow \exists a \exists k \in B (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u)$
50		ovex	$⊢ k \underset{˙}{\cdot} E \in V$
51		oveq1	$⊢ a = k \underset{˙}{\cdot} E \to a \underset{˙}{+} u = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
52	51	eqeq2d	$⊢ a = k \underset{˙}{\cdot} E \to (X = a \underset{˙}{+} u \leftrightarrow X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
53	50 52	ceqsexv	$⊢ \exists a (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u) \leftrightarrow X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
54	53	rexbii	$⊢ \exists k \in B \exists a (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u) \leftrightarrow \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
55	49 54	bitr3i	$⊢ \exists a \exists k \in B (a = k \underset{˙}{\cdot} E \land X = a \underset{˙}{+} u) \leftrightarrow \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
56	48 55	bitrdi	$⊢ φ \to (\exists a (a \in N (\{E\}) \land X = a \underset{˙}{+} u) \leftrightarrow \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
57	42 56	bitrid	$⊢ φ \to (\exists a \in N (\{E\}) X = a \underset{˙}{+} u \leftrightarrow \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
58	57	rexbidv	$⊢ φ \to (\exists u \in O (\{E\}) \exists a \in N (\{E\}) X = a \underset{˙}{+} u \leftrightarrow \exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
59	41 58	bitrid	$⊢ φ \to (\exists a \in N (\{E\}) \exists u \in O (\{E\}) X = a \underset{˙}{+} u \leftrightarrow \exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
60	40 59	mpbid	$⊢ φ \to \exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$

Metamath Proof Explorer

Theorem hdmapglem7a

Proof