lcfrlem6

Description: Lemma for lcfr . Closure of vector sum with colinear vectors. TODO: Move down N definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem6.h	$⊢ H = LHyp (K)$
	lcfrlem6.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem6.u	$⊢ U = DVecH (K) (W)$
	lcfrlem6.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem6.n	$⊢ N = LSpan (U)$
	lcfrlem6.l	$⊢ L = LKer (U)$
	lcfrlem6.d	$⊢ D = LDual (U)$
	lcfrlem6.q	$⊢ Q = LSubSp (D)$
	lcfrlem6.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem6.g	$⊢ φ \to G \in Q$
	lcfrlem6.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
	lcfrlem6.x	$⊢ φ \to X \in E$
	lcfrlem6.y	$⊢ φ \to Y \in E$
	lcfrlem6.en	$⊢ φ \to N (\{X\}) = N (\{Y\})$
Assertion	lcfrlem6	$⊢ φ \to X \underset{˙}{+} Y \in E$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem6.h	$⊢ H = LHyp (K)$
2		lcfrlem6.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem6.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem6.p	$⊢ \underset{˙}{+} = +_{U}$
5		lcfrlem6.n	$⊢ N = LSpan (U)$
6		lcfrlem6.l	$⊢ L = LKer (U)$
7		lcfrlem6.d	$⊢ D = LDual (U)$
8		lcfrlem6.q	$⊢ Q = LSubSp (D)$
9		lcfrlem6.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem6.g	$⊢ φ \to G \in Q$
11		lcfrlem6.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
12		lcfrlem6.x	$⊢ φ \to X \in E$
13		lcfrlem6.y	$⊢ φ \to Y \in E$
14		lcfrlem6.en	$⊢ φ \to N (\{X\}) = N (\{Y\})$
15	12 11	eleqtrdi	$⊢ φ \to X \in ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
16		eliun	$⊢ X \in ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \leftrightarrow \exists g \in G X \in \underset{˙}{⊥} (L (g))$
17	15 16	sylib	$⊢ φ \to \exists g \in G X \in \underset{˙}{⊥} (L (g))$
18	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
19	18	adantr	$⊢ (φ \land g \in G) \to U \in LMod$
20	19	adantr	$⊢ ((φ \land g \in G) \land X \in \underset{˙}{⊥} (L (g))) \to U \in LMod$
21	9	adantr	$⊢ (φ \land g \in G) \to (K \in HL \land W \in H)$
22		eqid	$⊢ {Base}_{U} = {Base}_{U}$
23		eqid	$⊢ LFnl (U) = LFnl (U)$
24		eqid	$⊢ {Base}_{D} = {Base}_{D}$
25	24 8	lssel	$⊢ (G \in Q \land g \in G) \to g \in {Base}_{D}$
26	10 25	sylan	$⊢ (φ \land g \in G) \to g \in {Base}_{D}$
27	23 7 24 18	ldualvbase	$⊢ φ \to {Base}_{D} = LFnl (U)$
28	27	adantr	$⊢ (φ \land g \in G) \to {Base}_{D} = LFnl (U)$
29	26 28	eleqtrd	$⊢ (φ \land g \in G) \to g \in LFnl (U)$
30	22 23 6 19 29	lkrssv	$⊢ (φ \land g \in G) \to L (g) \subseteq {Base}_{U}$
31		eqid	$⊢ LSubSp (U) = LSubSp (U)$
32	1 3 22 31 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (g) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (g)) \in LSubSp (U)$
33	21 30 32	syl2anc	$⊢ (φ \land g \in G) \to \underset{˙}{⊥} (L (g)) \in LSubSp (U)$
34	33	adantr	$⊢ ((φ \land g \in G) \land X \in \underset{˙}{⊥} (L (g))) \to \underset{˙}{⊥} (L (g)) \in LSubSp (U)$
35		simpr	$⊢ ((φ \land g \in G) \land X \in \underset{˙}{⊥} (L (g))) \to X \in \underset{˙}{⊥} (L (g))$
36	14	adantr	$⊢ (φ \land g \in G) \to N (\{X\}) = N (\{Y\})$
37	36	adantr	$⊢ ((φ \land g \in G) \land N (\{X\}) \subseteq \underset{˙}{⊥} (L (g))) \to N (\{X\}) = N (\{Y\})$
38		simpr	$⊢ ((φ \land g \in G) \land N (\{X\}) \subseteq \underset{˙}{⊥} (L (g))) \to N (\{X\}) \subseteq \underset{˙}{⊥} (L (g))$
39	37 38	eqsstrrd	$⊢ ((φ \land g \in G) \land N (\{X\}) \subseteq \underset{˙}{⊥} (L (g))) \to N (\{Y\}) \subseteq \underset{˙}{⊥} (L (g))$
40	39	ex	$⊢ (φ \land g \in G) \to (N (\{X\}) \subseteq \underset{˙}{⊥} (L (g)) \to N (\{Y\}) \subseteq \underset{˙}{⊥} (L (g)))$
41	1 2 3 22 6 7 8 11 9 10 12	lcfrlem4	$⊢ φ \to X \in {Base}_{U}$
42	41	adantr	$⊢ (φ \land g \in G) \to X \in {Base}_{U}$
43	22 31 5 19 33 42	lspsnel5	$⊢ (φ \land g \in G) \to (X \in \underset{˙}{⊥} (L (g)) \leftrightarrow N (\{X\}) \subseteq \underset{˙}{⊥} (L (g)))$
44	1 2 3 22 6 7 8 11 9 10 13	lcfrlem4	$⊢ φ \to Y \in {Base}_{U}$
45	44	adantr	$⊢ (φ \land g \in G) \to Y \in {Base}_{U}$
46	22 31 5 19 33 45	lspsnel5	$⊢ (φ \land g \in G) \to (Y \in \underset{˙}{⊥} (L (g)) \leftrightarrow N (\{Y\}) \subseteq \underset{˙}{⊥} (L (g)))$
47	40 43 46	3imtr4d	$⊢ (φ \land g \in G) \to (X \in \underset{˙}{⊥} (L (g)) \to Y \in \underset{˙}{⊥} (L (g)))$
48	47	imp	$⊢ ((φ \land g \in G) \land X \in \underset{˙}{⊥} (L (g))) \to Y \in \underset{˙}{⊥} (L (g))$
49	4 31	lssvacl	$⊢ ((U \in LMod \land \underset{˙}{⊥} (L (g)) \in LSubSp (U)) \land (X \in \underset{˙}{⊥} (L (g)) \land Y \in \underset{˙}{⊥} (L (g)))) \to X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g))$
50	20 34 35 48 49	syl22anc	$⊢ ((φ \land g \in G) \land X \in \underset{˙}{⊥} (L (g))) \to X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g))$
51	50	ex	$⊢ (φ \land g \in G) \to (X \in \underset{˙}{⊥} (L (g)) \to X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g)))$
52	51	reximdva	$⊢ φ \to (\exists g \in G X \in \underset{˙}{⊥} (L (g)) \to \exists g \in G X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g)))$
53	17 52	mpd	$⊢ φ \to \exists g \in G X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g))$
54		eliun	$⊢ X \underset{˙}{+} Y \in ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \leftrightarrow \exists g \in G X \underset{˙}{+} Y \in \underset{˙}{⊥} (L (g))$
55	53 54	sylibr	$⊢ φ \to X \underset{˙}{+} Y \in ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
56	55 11	eleqtrrdi	$⊢ φ \to X \underset{˙}{+} Y \in E$

Metamath Proof Explorer

Theorem lcfrlem6

Proof