lclkrlem2s

Description: Lemma for lclkr . Thus, the sum has a closed kernel when B is zero. (Contributed by NM, 18-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\})$
	lclkrlem2q.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
	lclkrlem2q.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
	lclkrlem2r.bn	$⊢ φ \to B = 0_{U}$
Assertion	lclkrlem2s	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

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		lclkrlem2q.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
25		lclkrlem2q.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
26		lclkrlem2r.bn	$⊢ φ \to B = 0_{U}$
27	12	snssd	$⊢ φ \to \{Y\} \subseteq V$
28		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
29	17 28 19 1 18	dochcl	$⊢ ((K \in HL \land W \in H) \land \{Y\} \subseteq V) \to \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
30	21 27 29	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
31	17 28 18	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))) = \underset{˙}{⊥} (\{Y\})$
32	21 30 31	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))) = \underset{˙}{⊥} (\{Y\})$
33	32	ad2antrr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))) = \underset{˙}{⊥} (\{Y\})$
34	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 26	lclkrlem2r	$⊢ φ \to L (G) \subseteq L (E \underset{˙}{+} G)$
35	34	ad2antrr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (G) \subseteq L (E \underset{˙}{+} G)$
36		eqid	$⊢ LSHyp (U) = LSHyp (U)$
37	17 19 21	dvhlvec	$⊢ φ \to U \in LVec$
38	37	ad2antrr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to U \in LVec$
39		simplr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (G) \in LSHyp (U)$
40		simpr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E \underset{˙}{+} G) \in LSHyp (U)$
41	36 38 39 40	lshpcmp	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to (L (G) \subseteq L (E \underset{˙}{+} G) \leftrightarrow L (G) = L (E \underset{˙}{+} G))$
42	35 41	mpbid	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (G) = L (E \underset{˙}{+} G)$
43	23	ad2antrr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (G) = \underset{˙}{⊥} (\{Y\})$
44	42 43	eqtr3d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E \underset{˙}{+} G) = \underset{˙}{⊥} (\{Y\})$
45	44	fveq2d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))$
46	45	fveq2d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\})))$
47	33 46 44	3eqtr4d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
48	17 19 18 1 21	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
49	48	ad2antrr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
50		simpr	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) = V) \to L (E \underset{˙}{+} G) = V$
51	50	fveq2d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) = V) \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) = \underset{˙}{⊥} (V)$
52	51	fveq2d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
53	49 52 50	3eqtr4d	$⊢ ((φ \land L (G) \in LSHyp (U)) \land L (E \underset{˙}{+} G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
54	17 19 21	dvhlmod	$⊢ φ \to U \in LMod$
55	8 9 10 54 13 14	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
56	1 36 8 16 37 55	lkrshpor	$⊢ φ \to (L (E \underset{˙}{+} G) \in LSHyp (U) \lor L (E \underset{˙}{+} G) = V)$
57	56	adantr	$⊢ (φ \land L (G) \in LSHyp (U)) \to (L (E \underset{˙}{+} G) \in LSHyp (U) \lor L (E \underset{˙}{+} G) = V)$
58	47 53 57	mpjaodan	$⊢ (φ \land L (G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
59	48	adantr	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
60	1 8 16 54 55	lkrssv	$⊢ φ \to L (E \underset{˙}{+} G) \subseteq V$
61	60	adantr	$⊢ (φ \land L (G) = V) \to L (E \underset{˙}{+} G) \subseteq V$
62		simpr	$⊢ (φ \land L (G) = V) \to L (G) = V$
63	34	adantr	$⊢ (φ \land L (G) = V) \to L (G) \subseteq L (E \underset{˙}{+} G)$
64	62 63	eqsstrrd	$⊢ (φ \land L (G) = V) \to V \subseteq L (E \underset{˙}{+} G)$
65	61 64	eqssd	$⊢ (φ \land L (G) = V) \to L (E \underset{˙}{+} G) = V$
66	65	fveq2d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) = \underset{˙}{⊥} (V)$
67	66	fveq2d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
68	59 67 65	3eqtr4d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
69	1 36 8 16 37 14	lkrshpor	$⊢ φ \to (L (G) \in LSHyp (U) \lor L (G) = V)$
70	58 68 69	mpjaodan	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Metamath Proof Explorer

Theorem lclkrlem2s

Proof