lcfrlem40

Description: Lemma for lcfr . Eliminate B and I . (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\})$
Assertion	lcfrlem40	$⊢ φ \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		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
22	1 3 11	dvhlmod	$⊢ φ \to U \in LMod$
23		eqid	$⊢ {Base}_{U} = {Base}_{U}$
24	1 2 3 23 6 7 8 10 11 12 14	lcfrlem4	$⊢ φ \to X \in {Base}_{U}$
25		eldifsn	$⊢ X \in ({Base}_{U} ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in {Base}_{U} \land X \neq \underset{˙}{0})$
26	24 17 25	sylanbrc	$⊢ φ \to X \in ({Base}_{U} ∖ \{\underset{˙}{0}\})$
27	1 2 3 23 6 7 8 10 11 12 15	lcfrlem4	$⊢ φ \to Y \in {Base}_{U}$
28		eldifsn	$⊢ Y \in ({Base}_{U} ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in {Base}_{U} \land Y \neq \underset{˙}{0})$
29	27 18 28	sylanbrc	$⊢ φ \to Y \in ({Base}_{U} ∖ \{\underset{˙}{0}\})$
30	1 2 3 23 4 16 19 21 11 26 29 20	lcfrlem21	$⊢ φ \to N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSAtoms (U)$
31	16 21 22 30	lsateln0	$⊢ φ \to \exists i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) i \neq \underset{˙}{0}$
32	11	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
33	12	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to G \in Q$
34	13	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to G \subseteq C$
35	14	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to X \in E$
36	15	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to Y \in E$
37	17	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to X \neq \underset{˙}{0}$
38	18	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to Y \neq \underset{˙}{0}$
39	20	3ad2ant1	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y\})$
40		eqid	$⊢ N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
41		simp2	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}))$
42		simp3	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to i \neq \underset{˙}{0}$
43	1 2 3 4 5 6 7 8 9 10 32 33 34 35 36 16 37 38 19 39 40 41 42	lcfrlem39	$⊢ (φ \land i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) \land i \neq \underset{˙}{0}) \to X \underset{˙}{+} Y \in E$
44	43	rexlimdv3a	$⊢ φ \to (\exists i \in (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) i \neq \underset{˙}{0} \to X \underset{˙}{+} Y \in E)$
45	31 44	mpd	$⊢ φ \to X \underset{˙}{+} Y \in E$

Metamath Proof Explorer

Theorem lcfrlem40

Proof