lcfrlem35

	Ref	Expression
Hypotheses	lcfrlem17.h	$⊢ H = LHyp (K)$
	lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem17.u	$⊢ U = DVecH (K) (W)$
	lcfrlem17.v	$⊢ V = {Base}_{U}$
	lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfrlem17.n	$⊢ N = LSpan (U)$
	lcfrlem17.a	$⊢ A = LSAtoms (U)$
	lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
	lcfrlem24.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfrlem24.s	$⊢ S = Scalar (U)$
	lcfrlem24.q	$⊢ Q = 0_{S}$
	lcfrlem24.r	$⊢ R = {Base}_{S}$
	lcfrlem24.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))))$
	lcfrlem24.ib	$⊢ φ \to I \in B$
	lcfrlem24.l	$⊢ L = LKer (U)$
	lcfrlem25.d	$⊢ D = LDual (U)$
	lcfrlem28.jn	$⊢ φ \to J (Y) (I) \neq Q$
	lcfrlem29.i	$⊢ F = {inv}_{r} (S)$
	lcfrlem30.m	$⊢ \underset{˙}{-} = -_{D}$
	lcfrlem30.c	$⊢ C = J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
Assertion	lcfrlem35	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (C)$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$⊢ H = LHyp (K)$
2		lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem17.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem17.v	$⊢ V = {Base}_{U}$
5		lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
6		lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
7		lcfrlem17.n	$⊢ N = LSpan (U)$
8		lcfrlem17.a	$⊢ A = LSAtoms (U)$
9		lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
11		lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
12		lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
13		lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
14		lcfrlem24.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
15		lcfrlem24.s	$⊢ S = Scalar (U)$
16		lcfrlem24.q	$⊢ Q = 0_{S}$
17		lcfrlem24.r	$⊢ R = {Base}_{S}$
18		lcfrlem24.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))))$
19		lcfrlem24.ib	$⊢ φ \to I \in B$
20		lcfrlem24.l	$⊢ L = LKer (U)$
21		lcfrlem25.d	$⊢ D = LDual (U)$
22		lcfrlem28.jn	$⊢ φ \to J (Y) (I) \neq Q$
23		lcfrlem29.i	$⊢ F = {inv}_{r} (S)$
24		lcfrlem30.m	$⊢ \underset{˙}{-} = -_{D}$
25		lcfrlem30.c	$⊢ C = J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
26		eqid	$⊢ LSSum (U) = LSSum (U)$
27	1 2 3 4 5 6 7 8 9 10 11 12 13 26	lcfrlem23	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B = \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
28	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	lcfrlem24	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) = L (J (X)) \cap L (J (Y))$
29		eqid	$⊢ \cdot_{S} = \cdot_{S}$
30		eqid	$⊢ LFnl (U) = LFnl (U)$
31		eqid	$⊢ \cdot_{D} = \cdot_{D}$
32	1 3 9	dvhlvec	$⊢ φ \to U \in LVec$
33		eqid	$⊢ 0_{D} = 0_{D}$
34		eqid	$⊢ \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
35	1 2 3 4 5 14 15 17 6 30 20 21 33 34 18 9 10	lcfrlem10	$⊢ φ \to J (X) \in LFnl (U)$
36	1 2 3 4 5 14 15 17 6 30 20 21 33 34 18 9 11	lcfrlem10	$⊢ φ \to J (Y) \in LFnl (U)$
37		eqid	$⊢ LSubSp (U) = LSubSp (U)$
38	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
39	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$⊢ φ \to B \in A$
40	37 8 38 39	lsatlssel	$⊢ φ \to B \in LSubSp (U)$
41	4 37	lssel	$⊢ (B \in LSubSp (U) \land I \in B) \to I \in V$
42	40 19 41	syl2anc	$⊢ φ \to I \in V$
43	4 15 29 16 23 30 21 31 24 32 35 36 42 22 25 20	lcfrlem2	$⊢ φ \to L (J (X)) \cap L (J (Y)) \subseteq L (C)$
44	28 43	eqsstrd	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \subseteq L (C)$
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22	lcfrlem28	$⊢ φ \to I \neq \underset{˙}{0}$
46	6 7 8 32 39 19 45	lsatel	$⊢ φ \to B = N (\{I\})$
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	lcfrlem30	$⊢ φ \to C \in LFnl (U)$
48	30 20 37	lkrlss	$⊢ (U \in LMod \land C \in LFnl (U)) \to L (C) \in LSubSp (U)$
49	38 47 48	syl2anc	$⊢ φ \to L (C) \in LSubSp (U)$
50	4 15 29 16 23 30 21 31 24 32 35 36 42 22 25 20	lcfrlem3	$⊢ φ \to I \in L (C)$
51	37 7 38 49 50	ellspsn5	$⊢ φ \to N (\{I\}) \subseteq L (C)$
52	46 51	eqsstrd	$⊢ φ \to B \subseteq L (C)$
53	37	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
54	38 53	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
55	10	eldifad	$⊢ φ \to X \in V$
56	11	eldifad	$⊢ φ \to Y \in V$
57		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
58	55 56 57	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
59	1 3 4 37 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \{X, Y\} \subseteq V) \to \underset{˙}{⊥} (\{X, Y\}) \in LSubSp (U)$
60	9 58 59	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \in LSubSp (U)$
61	54 60	sseldd	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \in SubGrp (U)$
62	54 40	sseldd	$⊢ φ \to B \in SubGrp (U)$
63	54 49	sseldd	$⊢ φ \to L (C) \in SubGrp (U)$
64	26	lsmlub	$⊢ (\underset{˙}{⊥} (\{X, Y\}) \in SubGrp (U) \land B \in SubGrp (U) \land L (C) \in SubGrp (U)) \to ((\underset{˙}{⊥} (\{X, Y\}) \subseteq L (C) \land B \subseteq L (C)) \leftrightarrow \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (C))$
65	61 62 63 64	syl3anc	$⊢ φ \to ((\underset{˙}{⊥} (\{X, Y\}) \subseteq L (C) \land B \subseteq L (C)) \leftrightarrow \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (C))$
66	44 52 65	mpbi2and	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (C)$
67	27 66	eqsstrrd	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \subseteq L (C)$
68		eqid	$⊢ LSHyp (U) = LSHyp (U)$
69	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem17	$⊢ φ \to X \underset{˙}{+} Y \in (V ∖ \{\underset{˙}{0}\})$
70	1 2 3 4 6 68 9 69	dochsnshp	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSHyp (U)$
71	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	lcfrlem34	$⊢ φ \to C \neq 0_{D}$
72	68 30 20 21 33 32 47	lduallkr3	$⊢ φ \to (L (C) \in LSHyp (U) \leftrightarrow C \neq 0_{D})$
73	71 72	mpbird	$⊢ φ \to L (C) \in LSHyp (U)$
74	68 32 70 73	lshpcmp	$⊢ φ \to (\underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \subseteq L (C) \leftrightarrow \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (C))$
75	67 74	mpbid	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (C)$

Metamath Proof Explorer

Theorem lcfrlem35

Proof