lcfrlem38

Description: Lemma for lcfr . Combine lcfrlem27 and lcfrlem37 . (Contributed by NM, 11-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem38.h	$⊢ H = LHyp (K)$
	lcfrlem38.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem38.u	$⊢ U = DVecH (K) (W)$
	lcfrlem38.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem38.f	$⊢ F = LFnl (U)$
	lcfrlem38.l	$⊢ L = LKer (U)$
	lcfrlem38.d	$⊢ D = LDual (U)$
	lcfrlem38.q	$⊢ Q = LSubSp (D)$
	lcfrlem38.c	$⊢ C = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfrlem38.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
	lcfrlem38.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem38.g	$⊢ φ \to G \in Q$
	lcfrlem38.gs	$⊢ φ \to G \subseteq C$
	lcfrlem38.xe	$⊢ φ \to X \in E$
	lcfrlem38.ye	$⊢ φ \to Y \in E$
	lcfrlem38.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfrlem38.x	$⊢ φ \to X \neq \underset{˙}{0}$
	lcfrlem38.y	$⊢ φ \to Y \neq \underset{˙}{0}$
	lcfrlem38.sp	$⊢ N = LSpan (U)$
	lcfrlem38.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	lcfrlem38.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
	lcfrlem38.i	$⊢ φ \to I \in B$
	lcfrlem38.n	$⊢ φ \to I \neq \underset{˙}{0}$
	lcfrlem38.v	$⊢ V = {Base}_{U}$
	lcfrlem38.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfrlem38.s	$⊢ S = Scalar (U)$
	lcfrlem38.r	$⊢ R = {Base}_{S}$
	lcfrlem38.j	$⊢ J = (x \in (V ∖ \{\underset{˙}{0}\}) ⟼ (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
Assertion	lcfrlem38	$⊢ φ \to X \underset{˙}{+} Y \in E$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem38.h	$⊢ H = LHyp (K)$
2		lcfrlem38.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem38.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem38.p	$⊢ \underset{˙}{+} = +_{U}$
5		lcfrlem38.f	$⊢ F = LFnl (U)$
6		lcfrlem38.l	$⊢ L = LKer (U)$
7		lcfrlem38.d	$⊢ D = LDual (U)$
8		lcfrlem38.q	$⊢ Q = LSubSp (D)$
9		lcfrlem38.c	$⊢ C = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
10		lcfrlem38.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
11		lcfrlem38.k	$⊢ φ \to (K \in HL \land W \in H)$
12		lcfrlem38.g	$⊢ φ \to G \in Q$
13		lcfrlem38.gs	$⊢ φ \to G \subseteq C$
14		lcfrlem38.xe	$⊢ φ \to X \in E$
15		lcfrlem38.ye	$⊢ φ \to Y \in E$
16		lcfrlem38.z	$⊢ \underset{˙}{0} = 0_{U}$
17		lcfrlem38.x	$⊢ φ \to X \neq \underset{˙}{0}$
18		lcfrlem38.y	$⊢ φ \to Y \neq \underset{˙}{0}$
19		lcfrlem38.sp	$⊢ N = LSpan (U)$
20		lcfrlem38.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
21		lcfrlem38.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
22		lcfrlem38.i	$⊢ φ \to I \in B$
23		lcfrlem38.n	$⊢ φ \to I \neq \underset{˙}{0}$
24		lcfrlem38.v	$⊢ V = {Base}_{U}$
25		lcfrlem38.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
26		lcfrlem38.s	$⊢ S = Scalar (U)$
27		lcfrlem38.r	$⊢ R = {Base}_{S}$
28		lcfrlem38.j	$⊢ J = (x \in (V ∖ \{\underset{˙}{0}\}) ⟼ (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
29		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
30	11	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to (K \in HL \land W \in H)$
31	1 2 3 24 6 7 8 10 11 12 14	lcfrlem4	$⊢ φ \to X \in V$
32		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
33	31 17 32	sylanbrc	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
34	33	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to X \in (V ∖ \{\underset{˙}{0}\})$
35	1 2 3 24 6 7 8 10 11 12 15	lcfrlem4	$⊢ φ \to Y \in V$
36		eldifsn	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in V \land Y \neq \underset{˙}{0})$
37	35 18 36	sylanbrc	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
38	37	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to Y \in (V ∖ \{\underset{˙}{0}\})$
39	20	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to N (\{X\}) \neq N (\{Y\})$
40		eqid	$⊢ 0_{S} = 0_{S}$
41	22	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to I \in B$
42		simpr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to J (Y) (I) = 0_{S}$
43	23	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to I \neq \underset{˙}{0}$
44	12 8	eleqtrdi	$⊢ φ \to G \in LSubSp (D)$
45	44	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to G \in LSubSp (D)$
46	13 9	sseqtrdi	$⊢ φ \to G \subseteq \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
47	46	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to G \subseteq \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
48	14	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to X \in E$
49	15	adantr	$⊢ (φ \land J (Y) (I) = 0_{S}) \to Y \in E$
50	1 2 3 24 4 16 19 29 30 34 38 39 21 25 26 40 27 28 41 6 7 42 43 45 47 10 48 49	lcfrlem27	$⊢ (φ \land J (Y) (I) = 0_{S}) \to X \underset{˙}{+} Y \in E$
51	11	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to (K \in HL \land W \in H)$
52	33	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to X \in (V ∖ \{\underset{˙}{0}\})$
53	37	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to Y \in (V ∖ \{\underset{˙}{0}\})$
54	20	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to N (\{X\}) \neq N (\{Y\})$
55	22	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to I \in B$
56		simpr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to J (Y) (I) \neq 0_{S}$
57		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
58		eqid	$⊢ -_{D} = -_{D}$
59		eqid	$⊢ J (X) -_{D} (({inv}_{r} (S) (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = J (X) -_{D} (({inv}_{r} (S) (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
60	44	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to G \in LSubSp (D)$
61	46	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to G \subseteq \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
62	14	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to X \in E$
63	15	adantr	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to Y \in E$
64	1 2 3 24 4 16 19 29 51 52 53 54 21 25 26 40 27 28 55 6 7 56 57 58 59 60 61 10 62 63	lcfrlem37	$⊢ (φ \land J (Y) (I) \neq 0_{S}) \to X \underset{˙}{+} Y \in E$
65	50 64	pm2.61dane	$⊢ φ \to X \underset{˙}{+} Y \in E$

Metamath Proof Explorer

Theorem lcfrlem38

Proof