lcfrlem25

Description: Lemma for lcfr . Special case of lcfrlem35 when ( ( JY )I ) is zero. (Contributed by NM, 11-Mar-2015)

	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)$
	lcfrlem25.jz	$⊢ φ \to J (Y) (I) = Q$
	lcfrlem25.in	$⊢ φ \to I \neq \underset{˙}{0}$
Assertion	lcfrlem25	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (J (Y))$

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		lcfrlem25.jz	$⊢ φ \to J (Y) (I) = Q$
23		lcfrlem25.in	$⊢ φ \to I \neq \underset{˙}{0}$
24		eqid	$⊢ LSSum (U) = LSSum (U)$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 24	lcfrlem23	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B = \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
26	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))$
27		inss2	$⊢ L (J (X)) \cap L (J (Y)) \subseteq L (J (Y))$
28	26 27	eqsstrdi	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \subseteq L (J (Y))$
29	1 3 9	dvhlvec	$⊢ φ \to U \in LVec$
30	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$⊢ φ \to B \in A$
31	6 7 8 29 30 19 23	lsatel	$⊢ φ \to B = N (\{I\})$
32		eqid	$⊢ LSubSp (U) = LSubSp (U)$
33	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
34		eqid	$⊢ LFnl (U) = LFnl (U)$
35		eqid	$⊢ 0_{D} = 0_{D}$
36		eqid	$⊢ \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
37	1 2 3 4 5 14 15 17 6 34 20 21 35 36 18 9 11	lcfrlem10	$⊢ φ \to J (Y) \in LFnl (U)$
38	34 20 32	lkrlss	$⊢ (U \in LMod \land J (Y) \in LFnl (U)) \to L (J (Y)) \in LSubSp (U)$
39	33 37 38	syl2anc	$⊢ φ \to L (J (Y)) \in LSubSp (U)$
40	4 8 33 30	lsatssv	$⊢ φ \to B \subseteq V$
41	40 19	sseldd	$⊢ φ \to I \in V$
42	4 15 16 34 20 33 37 41	ellkr2	$⊢ φ \to (I \in L (J (Y)) \leftrightarrow J (Y) (I) = Q)$
43	22 42	mpbird	$⊢ φ \to I \in L (J (Y))$
44	32 7 33 39 43	ellspsn5	$⊢ φ \to N (\{I\}) \subseteq L (J (Y))$
45	31 44	eqsstrd	$⊢ φ \to B \subseteq L (J (Y))$
46	32	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
47	33 46	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
48	10	eldifad	$⊢ φ \to X \in V$
49	11	eldifad	$⊢ φ \to Y \in V$
50		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
51	48 49 50	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
52	1 3 4 32 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \{X, Y\} \subseteq V) \to \underset{˙}{⊥} (\{X, Y\}) \in LSubSp (U)$
53	9 51 52	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \in LSubSp (U)$
54	47 53	sseldd	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \in SubGrp (U)$
55	4 32 7 33 48 49	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
56	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem17	$⊢ φ \to X \underset{˙}{+} Y \in (V ∖ \{\underset{˙}{0}\})$
57	56	eldifad	$⊢ φ \to X \underset{˙}{+} Y \in V$
58	57	snssd	$⊢ φ \to \{X \underset{˙}{+} Y\} \subseteq V$
59	1 3 4 32 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \{X \underset{˙}{+} Y\} \subseteq V) \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
60	9 58 59	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
61	32	lssincl	$⊢ (U \in LMod \land N (\{X, Y\}) \in LSubSp (U) \land \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSubSp (U)) \to N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
62	33 55 60 61	syl3anc	$⊢ φ \to N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
63	13 62	eqeltrid	$⊢ φ \to B \in LSubSp (U)$
64	47 63	sseldd	$⊢ φ \to B \in SubGrp (U)$
65	47 39	sseldd	$⊢ φ \to L (J (Y)) \in SubGrp (U)$
66	24	lsmlub	$⊢ (\underset{˙}{⊥} (\{X, Y\}) \in SubGrp (U) \land B \in SubGrp (U) \land L (J (Y)) \in SubGrp (U)) \to ((\underset{˙}{⊥} (\{X, Y\}) \subseteq L (J (Y)) \land B \subseteq L (J (Y))) \leftrightarrow \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (J (Y)))$
67	54 64 65 66	syl3anc	$⊢ φ \to ((\underset{˙}{⊥} (\{X, Y\}) \subseteq L (J (Y)) \land B \subseteq L (J (Y))) \leftrightarrow \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (J (Y)))$
68	28 45 67	mpbi2and	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) LSSum (U) B \subseteq L (J (Y))$
69	25 68	eqsstrrd	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \subseteq L (J (Y))$
70		eqid	$⊢ LSHyp (U) = LSHyp (U)$
71	1 2 3 4 6 70 9 56	dochsnshp	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in LSHyp (U)$
72	1 2 3 4 5 14 15 17 6 34 20 21 35 36 18 9 11	lcfrlem13	$⊢ φ \to J (Y) \in (\{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} ∖ \{0_{D}\})$
73		eldifsni	$⊢ J (Y) \in (\{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} ∖ \{0_{D}\}) \to J (Y) \neq 0_{D}$
74	72 73	syl	$⊢ φ \to J (Y) \neq 0_{D}$
75	70 34 20 21 35 29 37	lduallkr3	$⊢ φ \to (L (J (Y)) \in LSHyp (U) \leftrightarrow J (Y) \neq 0_{D})$
76	74 75	mpbird	$⊢ φ \to L (J (Y)) \in LSHyp (U)$
77	70 29 71 76	lshpcmp	$⊢ φ \to (\underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \subseteq L (J (Y)) \leftrightarrow \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (J (Y)))$
78	69 77	mpbid	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) = L (J (Y))$

Metamath Proof Explorer

Theorem lcfrlem25

Proof