lclkrlem2e

Description: Lemma for lclkr . The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2e.h	$⊢ H = LHyp (K)$
	lclkrlem2e.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2e.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2e.v	$⊢ V = {Base}_{U}$
	lclkrlem2e.z	$⊢ \underset{˙}{0} = 0_{U}$
	lclkrlem2e.f	$⊢ F = LFnl (U)$
	lclkrlem2e.l	$⊢ L = LKer (U)$
	lclkrlem2e.d	$⊢ D = LDual (U)$
	lclkrlem2e.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2e.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2e.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2e.e	$⊢ φ \to E \in F$
	lclkrlem2e.g	$⊢ φ \to G \in F$
	lclkrlem2e.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
	lclkrlem2e.ne	$⊢ φ \to L (E) = L (G)$
Assertion	lclkrlem2e	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2e.h	$⊢ H = LHyp (K)$
2		lclkrlem2e.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem2e.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem2e.v	$⊢ V = {Base}_{U}$
5		lclkrlem2e.z	$⊢ \underset{˙}{0} = 0_{U}$
6		lclkrlem2e.f	$⊢ F = LFnl (U)$
7		lclkrlem2e.l	$⊢ L = LKer (U)$
8		lclkrlem2e.d	$⊢ D = LDual (U)$
9		lclkrlem2e.p	$⊢ \underset{˙}{+} = +_{D}$
10		lclkrlem2e.k	$⊢ φ \to (K \in HL \land W \in H)$
11		lclkrlem2e.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
12		lclkrlem2e.e	$⊢ φ \to E \in F$
13		lclkrlem2e.g	$⊢ φ \to G \in F$
14		lclkrlem2e.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
15		lclkrlem2e.ne	$⊢ φ \to L (E) = L (G)$
16	10	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to (K \in HL \land W \in H)$
17	11	eldifad	$⊢ φ \to X \in V$
18	17	snssd	$⊢ φ \to \{X\} \subseteq V$
19	18	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \{X\} \subseteq V$
20		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
21	1 20 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V) \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
22	16 19 21	syl2anc	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
23	1 20 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\{X\})$
24	16 22 23	syl2anc	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\{X\})$
25	14	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E) = \underset{˙}{⊥} (\{X\})$
26		inidm	$⊢ L (E) \cap L (E) = L (E)$
27	15	ineq2d	$⊢ φ \to L (E) \cap L (E) = L (E) \cap L (G)$
28	26 27	eqtr3id	$⊢ φ \to L (E) = L (E) \cap L (G)$
29	1 3 10	dvhlmod	$⊢ φ \to U \in LMod$
30	6 7 8 9 29 12 13	lkrin	$⊢ φ \to L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G)$
31	28 30	eqsstrd	$⊢ φ \to L (E) \subseteq L (E \underset{˙}{+} G)$
32	31	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E) \subseteq L (E \underset{˙}{+} G)$
33		eqid	$⊢ LSHyp (U) = LSHyp (U)$
34	1 3 10	dvhlvec	$⊢ φ \to U \in LVec$
35	34	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to U \in LVec$
36		eqid	$⊢ LSpan (U) = LSpan (U)$
37	1 3 2 4 36 10 18	dochocsp	$⊢ φ \to \underset{˙}{⊥} (LSpan (U) (\{X\})) = \underset{˙}{⊥} (\{X\})$
38	37	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (LSpan (U) (\{X\})) = \underset{˙}{⊥} (\{X\})$
39	25 38	eqtr4d	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E) = \underset{˙}{⊥} (LSpan (U) (\{X\}))$
40		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
41	4 36 5 40 29 11	lsatlspsn	$⊢ φ \to LSpan (U) (\{X\}) \in LSAtoms (U)$
42	41	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to LSpan (U) (\{X\}) \in LSAtoms (U)$
43	1 3 2 40 33 16 42	dochsatshp	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (LSpan (U) (\{X\})) \in LSHyp (U)$
44	39 43	eqeltrd	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E) \in LSHyp (U)$
45		simpr	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E \underset{˙}{+} G) \in LSHyp (U)$
46	33 35 44 45	lshpcmp	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to (L (E) \subseteq L (E \underset{˙}{+} G) \leftrightarrow L (E) = L (E \underset{˙}{+} G))$
47	32 46	mpbid	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to L (E) = L (E \underset{˙}{+} G)$
48	25 47	eqtr3d	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\{X\}) = L (E \underset{˙}{+} G)$
49	48	fveq2d	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{X\})) = \underset{˙}{⊥} (L (E \underset{˙}{+} G))$
50	49	fveq2d	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G)))$
51	24 50 48	3eqtr3d	$⊢ (φ \land L (E \underset{˙}{+} G) \in LSHyp (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
52	51	ex	$⊢ φ \to (L (E \underset{˙}{+} G) \in LSHyp (U) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G))$
53	1 3 2 4 10	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
54		2fveq3	$⊢ L (E \underset{˙}{+} G) = V \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
55		id	$⊢ L (E \underset{˙}{+} G) = V \to L (E \underset{˙}{+} G) = V$
56	54 55	eqeq12d	$⊢ L (E \underset{˙}{+} G) = V \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V)$
57	53 56	syl5ibrcom	$⊢ φ \to (L (E \underset{˙}{+} G) = V \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G))$
58	6 8 9 29 12 13	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
59	4 33 6 7 34 58	lkrshpor	$⊢ φ \to (L (E \underset{˙}{+} G) \in LSHyp (U) \lor L (E \underset{˙}{+} G) = V)$
60	52 57 59	mpjaod	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Metamath Proof Explorer

Theorem lclkrlem2e

Proof