lcfl9a

Description: Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	lcfl9a.h	$⊢ H = LHyp (K)$
	lcfl9a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfl9a.u	$⊢ U = DVecH (K) (W)$
	lcfl9a.v	$⊢ V = {Base}_{U}$
	lcfl9a.f	$⊢ F = LFnl (U)$
	lcfl9a.l	$⊢ L = LKer (U)$
	lcfl9a.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfl9a.g	$⊢ φ \to G \in F$
	lcfl9a.x	$⊢ φ \to X \in V$
	lcfl9a.s	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \subseteq L (G)$
Assertion	lcfl9a	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$

Proof

Step	Hyp	Ref	Expression
1		lcfl9a.h	$⊢ H = LHyp (K)$
2		lcfl9a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfl9a.u	$⊢ U = DVecH (K) (W)$
4		lcfl9a.v	$⊢ V = {Base}_{U}$
5		lcfl9a.f	$⊢ F = LFnl (U)$
6		lcfl9a.l	$⊢ L = LKer (U)$
7		lcfl9a.k	$⊢ φ \to (K \in HL \land W \in H)$
8		lcfl9a.g	$⊢ φ \to G \in F$
9		lcfl9a.x	$⊢ φ \to X \in V$
10		lcfl9a.s	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \subseteq L (G)$
11	1 3 2 4 7	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
12	11	adantr	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
13	1 3 7	dvhlmod	$⊢ φ \to U \in LMod$
14	4 5 6 13 8	lkrssv	$⊢ φ \to L (G) \subseteq V$
15	14	adantr	$⊢ (φ \land X = 0_{U}) \to L (G) \subseteq V$
16		sneq	$⊢ X = 0_{U} \to \{X\} = \{0_{U}\}$
17	16	fveq2d	$⊢ X = 0_{U} \to \underset{˙}{⊥} (\{X\}) = \underset{˙}{⊥} (\{0_{U}\})$
18		eqid	$⊢ 0_{U} = 0_{U}$
19	1 3 2 4 18	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{0_{U}\}) = V$
20	7 19	syl	$⊢ φ \to \underset{˙}{⊥} (\{0_{U}\}) = V$
21	17 20	sylan9eqr	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (\{X\}) = V$
22	10	adantr	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (\{X\}) \subseteq L (G)$
23	21 22	eqsstrrd	$⊢ (φ \land X = 0_{U}) \to V \subseteq L (G)$
24	15 23	eqssd	$⊢ (φ \land X = 0_{U}) \to L (G) = V$
25	24	fveq2d	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (V)$
26	25	fveq2d	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
27	12 26 24	3eqtr4d	$⊢ (φ \land X = 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
28	11	adantr	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
29		simpr	$⊢ (φ \land L (G) = V) \to L (G) = V$
30	29	fveq2d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (V)$
31	30	fveq2d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
32	28 31 29	3eqtr4d	$⊢ (φ \land L (G) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
33	9	snssd	$⊢ φ \to \{X\} \subseteq V$
34		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
35	1 34 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V) \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
36	7 33 35	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
37	1 34 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\{X\})$
38	7 36 37	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\{X\})$
39	38	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\{X\})$
40	10	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\{X\}) \subseteq L (G)$
41		eqid	$⊢ LSHyp (U) = LSHyp (U)$
42	1 3 7	dvhlvec	$⊢ φ \to U \in LVec$
43	42	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to U \in LVec$
44	7	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to (K \in HL \land W \in H)$
45	9	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to X \in V$
46		simprl	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to X \neq 0_{U}$
47		eldifsn	$⊢ X \in (V ∖ \{0_{U}\}) \leftrightarrow (X \in V \land X \neq 0_{U})$
48	45 46 47	sylanbrc	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to X \in (V ∖ \{0_{U}\})$
49	1 2 3 4 18 41 44 48	dochsnshp	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\{X\}) \in LSHyp (U)$
50		simprr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to L (G) \neq V$
51	4 41 5 6 42 8	lkrshp4	$⊢ φ \to (L (G) \neq V \leftrightarrow L (G) \in LSHyp (U))$
52	51	adantr	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to (L (G) \neq V \leftrightarrow L (G) \in LSHyp (U))$
53	50 52	mpbid	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to L (G) \in LSHyp (U)$
54	41 43 49 53	lshpcmp	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to (\underset{˙}{⊥} (\{X\}) \subseteq L (G) \leftrightarrow \underset{˙}{⊥} (\{X\}) = L (G))$
55	40 54	mpbid	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\{X\}) = L (G)$
56	55	fveq2d	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{X\})) = \underset{˙}{⊥} (L (G))$
57	56	fveq2d	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{X\}))) = \underset{˙}{⊥} (\underset{˙}{⊥} (L (G)))$
58	39 57 55	3eqtr3d	$⊢ (φ \land (X \neq 0_{U} \land L (G) \neq V)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
59	27 32 58	pm2.61da2ne	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$

Metamath Proof Explorer

Theorem lcfl9a

Proof