lclkrlem2v

Description: Lemma for lclkr . When the hypotheses of lclkrlem2u and lclkrlem2u are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid , which requires the orthomodular law dihoml4 (Lemma 3.3 of Holland95 p. 214). (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	$⊢ V = {Base}_{U}$
	lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lclkrlem2m.s	$⊢ S = Scalar (U)$
	lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
	lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
	lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
	lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
	lclkrlem2m.f	$⊢ F = LFnl (U)$
	lclkrlem2m.d	$⊢ D = LDual (U)$
	lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2m.x	$⊢ φ \to X \in V$
	lclkrlem2m.y	$⊢ φ \to Y \in V$
	lclkrlem2m.e	$⊢ φ \to E \in F$
	lclkrlem2m.g	$⊢ φ \to G \in F$
	lclkrlem2n.n	$⊢ N = LSpan (U)$
	lclkrlem2n.l	$⊢ L = LKer (U)$
	lclkrlem2o.h	$⊢ H = LHyp (K)$
	lclkrlem2o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2o.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2o.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2o.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2q.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
	lclkrlem2q.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
	lclkrlem2v.j	$⊢ φ \to (E \underset{˙}{+} G) (X) = \underset{˙}{0}$
	lclkrlem2v.k	$⊢ φ \to (E \underset{˙}{+} G) (Y) = \underset{˙}{0}$
Assertion	lclkrlem2v	$⊢ φ \to L (E \underset{˙}{+} G) = V$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	$⊢ V = {Base}_{U}$
2		lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
3		lclkrlem2m.s	$⊢ S = Scalar (U)$
4		lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
5		lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
6		lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
7		lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
8		lclkrlem2m.f	$⊢ F = LFnl (U)$
9		lclkrlem2m.d	$⊢ D = LDual (U)$
10		lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
11		lclkrlem2m.x	$⊢ φ \to X \in V$
12		lclkrlem2m.y	$⊢ φ \to Y \in V$
13		lclkrlem2m.e	$⊢ φ \to E \in F$
14		lclkrlem2m.g	$⊢ φ \to G \in F$
15		lclkrlem2n.n	$⊢ N = LSpan (U)$
16		lclkrlem2n.l	$⊢ L = LKer (U)$
17		lclkrlem2o.h	$⊢ H = LHyp (K)$
18		lclkrlem2o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
19		lclkrlem2o.u	$⊢ U = DVecH (K) (W)$
20		lclkrlem2o.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
21		lclkrlem2o.k	$⊢ φ \to (K \in HL \land W \in H)$
22		lclkrlem2q.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
23		lclkrlem2q.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
24		lclkrlem2v.j	$⊢ φ \to (E \underset{˙}{+} G) (X) = \underset{˙}{0}$
25		lclkrlem2v.k	$⊢ φ \to (E \underset{˙}{+} G) (Y) = \underset{˙}{0}$
26	17 19 21	dvhlmod	$⊢ φ \to U \in LMod$
27	8 9 10 26 13 14	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
28	1 8 16 26 27	lkrssv	$⊢ φ \to L (E \underset{˙}{+} G) \subseteq V$
29		eqid	$⊢ LSubSp (U) = LSubSp (U)$
30	1 29 15 26 11 12	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
31		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
32	17 19 1 15 31 21 11 12	dihprrn	$⊢ φ \to N (\{X, Y\}) \in ran DIsoH (K) (W)$
33	1 29	lssss	$⊢ N (\{X, Y\}) \in LSubSp (U) \to N (\{X, Y\}) \subseteq V$
34	30 33	syl	$⊢ φ \to N (\{X, Y\}) \subseteq V$
35	17 31 19 1 18 21 34	dochoccl	$⊢ φ \to (N (\{X, Y\}) \in ran DIsoH (K) (W) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (N (\{X, Y\}))) = N (\{X, Y\}))$
36	32 35	mpbid	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (N (\{X, Y\}))) = N (\{X, Y\})$
37	17 18 19 1 29 20 21 30 36	dochexmid	$⊢ φ \to N (\{X, Y\}) \underset{˙}{\oplus} \underset{˙}{⊥} (N (\{X, Y\})) = V$
38	17 19 21	dvhlvec	$⊢ φ \to U \in LVec$
39	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38 24 25	lclkrlem2n	$⊢ φ \to N (\{X, Y\}) \subseteq L (E \underset{˙}{+} G)$
40	11	snssd	$⊢ φ \to \{X\} \subseteq V$
41	12	snssd	$⊢ φ \to \{Y\} \subseteq V$
42	17 19 1 18	dochdmj1	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
43	21 40 41 42	syl3anc	$⊢ φ \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
44		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
45	44	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
46	45	fveq2i	$⊢ \underset{˙}{⊥} (N (\{X, Y\})) = \underset{˙}{⊥} (N (\{X\} \cup \{Y\}))$
47	40 41	unssd	$⊢ φ \to \{X\} \cup \{Y\} \subseteq V$
48	17 19 18 1 15 21 47	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X\} \cup \{Y\})) = \underset{˙}{⊥} (\{X\} \cup \{Y\})$
49	46 48	syl5eq	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) = \underset{˙}{⊥} (\{X\} \cup \{Y\})$
50	22 23	ineq12d	$⊢ φ \to L (E) \cap L (G) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
51	43 49 50	3eqtr4d	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) = L (E) \cap L (G)$
52	8 16 9 10 26 13 14	lkrin	$⊢ φ \to L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G)$
53	51 52	eqsstrd	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G)$
54	29	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
55	26 54	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
56	55 30	sseldd	$⊢ φ \to N (\{X, Y\}) \in SubGrp (U)$
57	17 19 1 29 18	dochlss	$⊢ ((K \in HL \land W \in H) \land N (\{X, Y\}) \subseteq V) \to \underset{˙}{⊥} (N (\{X, Y\})) \in LSubSp (U)$
58	21 34 57	syl2anc	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \in LSubSp (U)$
59	55 58	sseldd	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \in SubGrp (U)$
60	8 16 29	lkrlss	$⊢ (U \in LMod \land E \underset{˙}{+} G \in F) \to L (E \underset{˙}{+} G) \in LSubSp (U)$
61	26 27 60	syl2anc	$⊢ φ \to L (E \underset{˙}{+} G) \in LSubSp (U)$
62	55 61	sseldd	$⊢ φ \to L (E \underset{˙}{+} G) \in SubGrp (U)$
63	20	lsmlub	$⊢ (N (\{X, Y\}) \in SubGrp (U) \land \underset{˙}{⊥} (N (\{X, Y\})) \in SubGrp (U) \land L (E \underset{˙}{+} G) \in SubGrp (U)) \to ((N (\{X, Y\}) \subseteq L (E \underset{˙}{+} G) \land \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G)) \leftrightarrow N (\{X, Y\}) \underset{˙}{\oplus} \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G))$
64	56 59 62 63	syl3anc	$⊢ φ \to ((N (\{X, Y\}) \subseteq L (E \underset{˙}{+} G) \land \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G)) \leftrightarrow N (\{X, Y\}) \underset{˙}{\oplus} \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G))$
65	39 53 64	mpbi2and	$⊢ φ \to N (\{X, Y\}) \underset{˙}{\oplus} \underset{˙}{⊥} (N (\{X, Y\})) \subseteq L (E \underset{˙}{+} G)$
66	37 65	eqsstrrd	$⊢ φ \to V \subseteq L (E \underset{˙}{+} G)$
67	28 66	eqssd	$⊢ φ \to L (E \underset{˙}{+} G) = V$

Metamath Proof Explorer

Theorem lclkrlem2v

Proof