lclkrlem2f

Description: Lemma for lclkr . Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2f.h	$⊢ H = LHyp (K)$
	lclkrlem2f.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2f.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2f.v	$⊢ V = {Base}_{U}$
	lclkrlem2f.s	$⊢ S = Scalar (U)$
	lclkrlem2f.q	$⊢ Q = 0_{S}$
	lclkrlem2f.z	$⊢ \underset{˙}{0} = 0_{U}$
	lclkrlem2f.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2f.n	$⊢ N = LSpan (U)$
	lclkrlem2f.f	$⊢ F = LFnl (U)$
	lclkrlem2f.j	$⊢ J = LSHyp (U)$
	lclkrlem2f.l	$⊢ L = LKer (U)$
	lclkrlem2f.d	$⊢ D = LDual (U)$
	lclkrlem2f.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2f.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2f.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2f.e	$⊢ φ \to E \in F$
	lclkrlem2f.g	$⊢ φ \to G \in F$
	lclkrlem2f.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
	lclkrlem2f.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
	lclkrlem2f.kb	$⊢ φ \to (E \underset{˙}{+} G) (B) = Q$
	lclkrlem2f.nx	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
	lclkrlem2f.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2f.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2f.ne	$⊢ φ \to L (E) \neq L (G)$
	lclkrlem2f.lp	$⊢ φ \to L (E \underset{˙}{+} G) \in J$
Assertion	lclkrlem2f	$⊢ φ \to (L (E) \cap L (G)) \underset{˙}{\oplus} N (\{B\}) \subseteq L (E \underset{˙}{+} G)$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2f.h	$⊢ H = LHyp (K)$
2		lclkrlem2f.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem2f.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem2f.v	$⊢ V = {Base}_{U}$
5		lclkrlem2f.s	$⊢ S = Scalar (U)$
6		lclkrlem2f.q	$⊢ Q = 0_{S}$
7		lclkrlem2f.z	$⊢ \underset{˙}{0} = 0_{U}$
8		lclkrlem2f.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		lclkrlem2f.n	$⊢ N = LSpan (U)$
10		lclkrlem2f.f	$⊢ F = LFnl (U)$
11		lclkrlem2f.j	$⊢ J = LSHyp (U)$
12		lclkrlem2f.l	$⊢ L = LKer (U)$
13		lclkrlem2f.d	$⊢ D = LDual (U)$
14		lclkrlem2f.p	$⊢ \underset{˙}{+} = +_{D}$
15		lclkrlem2f.k	$⊢ φ \to (K \in HL \land W \in H)$
16		lclkrlem2f.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
17		lclkrlem2f.e	$⊢ φ \to E \in F$
18		lclkrlem2f.g	$⊢ φ \to G \in F$
19		lclkrlem2f.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
20		lclkrlem2f.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
21		lclkrlem2f.kb	$⊢ φ \to (E \underset{˙}{+} G) (B) = Q$
22		lclkrlem2f.nx	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
23		lclkrlem2f.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
24		lclkrlem2f.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
25		lclkrlem2f.ne	$⊢ φ \to L (E) \neq L (G)$
26		lclkrlem2f.lp	$⊢ φ \to L (E \underset{˙}{+} G) \in J$
27	1 3 15	dvhlmod	$⊢ φ \to U \in LMod$
28	10 12 13 14 27 17 18	lkrin	$⊢ φ \to L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G)$
29		eqid	$⊢ LSubSp (U) = LSubSp (U)$
30	29 11 27 26	lshplss	$⊢ φ \to L (E \underset{˙}{+} G) \in LSubSp (U)$
31	10 13 14 27 17 18	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
32	16	eldifad	$⊢ φ \to B \in V$
33	4 5 6 10 12 27 31 32	ellkr2	$⊢ φ \to (B \in L (E \underset{˙}{+} G) \leftrightarrow (E \underset{˙}{+} G) (B) = Q)$
34	21 33	mpbird	$⊢ φ \to B \in L (E \underset{˙}{+} G)$
35	29 9 27 30 34	lspsnel5a	$⊢ φ \to N (\{B\}) \subseteq L (E \underset{˙}{+} G)$
36	29	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
37	27 36	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
38	10 12 29	lkrlss	$⊢ (U \in LMod \land E \in F) \to L (E) \in LSubSp (U)$
39	27 17 38	syl2anc	$⊢ φ \to L (E) \in LSubSp (U)$
40	10 12 29	lkrlss	$⊢ (U \in LMod \land G \in F) \to L (G) \in LSubSp (U)$
41	27 18 40	syl2anc	$⊢ φ \to L (G) \in LSubSp (U)$
42	29	lssincl	$⊢ (U \in LMod \land L (E) \in LSubSp (U) \land L (G) \in LSubSp (U)) \to L (E) \cap L (G) \in LSubSp (U)$
43	27 39 41 42	syl3anc	$⊢ φ \to L (E) \cap L (G) \in LSubSp (U)$
44	37 43	sseldd	$⊢ φ \to L (E) \cap L (G) \in SubGrp (U)$
45	4 29 9	lspsncl	$⊢ (U \in LMod \land B \in V) \to N (\{B\}) \in LSubSp (U)$
46	27 32 45	syl2anc	$⊢ φ \to N (\{B\}) \in LSubSp (U)$
47	37 46	sseldd	$⊢ φ \to N (\{B\}) \in SubGrp (U)$
48	37 30	sseldd	$⊢ φ \to L (E \underset{˙}{+} G) \in SubGrp (U)$
49	8	lsmlub	$⊢ (L (E) \cap L (G) \in SubGrp (U) \land N (\{B\}) \in SubGrp (U) \land L (E \underset{˙}{+} G) \in SubGrp (U)) \to ((L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G) \land N (\{B\}) \subseteq L (E \underset{˙}{+} G)) \leftrightarrow (L (E) \cap L (G)) \underset{˙}{\oplus} N (\{B\}) \subseteq L (E \underset{˙}{+} G))$
50	44 47 48 49	syl3anc	$⊢ φ \to ((L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G) \land N (\{B\}) \subseteq L (E \underset{˙}{+} G)) \leftrightarrow (L (E) \cap L (G)) \underset{˙}{\oplus} N (\{B\}) \subseteq L (E \underset{˙}{+} G))$
51	28 35 50	mpbi2and	$⊢ φ \to (L (E) \cap L (G)) \underset{˙}{\oplus} N (\{B\}) \subseteq L (E \underset{˙}{+} G)$

Metamath Proof Explorer

Theorem lclkrlem2f

Proof