lcfl8b

Description: Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	lcfl8b.h	$⊢ H = LHyp (K)$
	lcfl8b.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfl8b.u	$⊢ U = DVecH (K) (W)$
	lcfl8b.v	$⊢ V = {Base}_{U}$
	lcfl8b.n	$⊢ N = LSpan (U)$
	lcfl8b.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfl8b.f	$⊢ F = LFnl (U)$
	lcfl8b.l	$⊢ L = LKer (U)$
	lcfl8b.d	$⊢ D = LDual (U)$
	lcfl8b.y	$⊢ Y = 0_{D}$
	lcfl8b.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfl8b.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfl8b.g	$⊢ φ \to G \in (C ∖ \{Y\})$
Assertion	lcfl8b	$⊢ φ \to \exists x \in (V ∖ \{\underset{˙}{0}\}) \underset{˙}{⊥} (L (G)) = N (\{x\})$

Proof

Step	Hyp	Ref	Expression
1		lcfl8b.h	$⊢ H = LHyp (K)$
2		lcfl8b.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfl8b.u	$⊢ U = DVecH (K) (W)$
4		lcfl8b.v	$⊢ V = {Base}_{U}$
5		lcfl8b.n	$⊢ N = LSpan (U)$
6		lcfl8b.z	$⊢ \underset{˙}{0} = 0_{U}$
7		lcfl8b.f	$⊢ F = LFnl (U)$
8		lcfl8b.l	$⊢ L = LKer (U)$
9		lcfl8b.d	$⊢ D = LDual (U)$
10		lcfl8b.y	$⊢ Y = 0_{D}$
11		lcfl8b.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
12		lcfl8b.k	$⊢ φ \to (K \in HL \land W \in H)$
13		lcfl8b.g	$⊢ φ \to G \in (C ∖ \{Y\})$
14	13	eldifad	$⊢ φ \to G \in C$
15	11	lcfl1lem	$⊢ G \in C \leftrightarrow (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
16	15	simplbi	$⊢ G \in C \to G \in F$
17	14 16	syl	$⊢ φ \to G \in F$
18	1 2 3 4 7 8 11 12 17	lcfl8	$⊢ φ \to (G \in C \leftrightarrow \exists x \in V L (G) = \underset{˙}{⊥} (\{x\}))$
19	14 18	mpbid	$⊢ φ \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\})$
20		fveq2	$⊢ L (G) = \underset{˙}{⊥} (\{x\}) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))$
21	20	adantl	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))$
22	12	ad2antrr	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to (K \in HL \land W \in H)$
23		simplr	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to x \in V$
24	1 3 2 4 5 22 23	dochocsn	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{x\})) = N (\{x\})$
25	21 24	eqtrd	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (L (G)) = N (\{x\})$
26	14 15	sylib	$⊢ φ \to (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
27	26	simprd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
28		eldifsni	$⊢ G \in (C ∖ \{Y\}) \to G \neq Y$
29	13 28	syl	$⊢ φ \to G \neq Y$
30	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
31	4 7 8 9 10 30 17	lkr0f2	$⊢ φ \to (L (G) = V \leftrightarrow G = Y)$
32	31	necon3bid	$⊢ φ \to (L (G) \neq V \leftrightarrow G \neq Y)$
33	29 32	mpbird	$⊢ φ \to L (G) \neq V$
34	27 33	eqnetrd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V$
35	34	ad2antrr	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V$
36		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
37	17	ad2antrr	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to G \in F$
38	1 2 3 4 36 7 8 22 37	dochkrsat2	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V \leftrightarrow \underset{˙}{⊥} (L (G)) \in LSAtoms (U))$
39	35 38	mpbid	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (L (G)) \in LSAtoms (U)$
40	25 39	eqeltrrd	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to N (\{x\}) \in LSAtoms (U)$
41	30	ad2antrr	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to U \in LMod$
42	4 5 6 36 41 23	lsatspn0	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to (N (\{x\}) \in LSAtoms (U) \leftrightarrow x \neq \underset{˙}{0})$
43	40 42	mpbid	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to x \neq \underset{˙}{0}$
44	43 25	jca	$⊢ ((φ \land x \in V) \land L (G) = \underset{˙}{⊥} (\{x\})) \to (x \neq \underset{˙}{0} \land \underset{˙}{⊥} (L (G)) = N (\{x\}))$
45	44	ex	$⊢ (φ \land x \in V) \to (L (G) = \underset{˙}{⊥} (\{x\}) \to (x \neq \underset{˙}{0} \land \underset{˙}{⊥} (L (G)) = N (\{x\})))$
46	45	reximdva	$⊢ φ \to (\exists x \in V L (G) = \underset{˙}{⊥} (\{x\}) \to \exists x \in V (x \neq \underset{˙}{0} \land \underset{˙}{⊥} (L (G)) = N (\{x\})))$
47	19 46	mpd	$⊢ φ \to \exists x \in V (x \neq \underset{˙}{0} \land \underset{˙}{⊥} (L (G)) = N (\{x\}))$
48		rexdifsn	$⊢ \exists x \in (V ∖ \{\underset{˙}{0}\}) \underset{˙}{⊥} (L (G)) = N (\{x\}) \leftrightarrow \exists x \in V (x \neq \underset{˙}{0} \land \underset{˙}{⊥} (L (G)) = N (\{x\}))$
49	47 48	sylibr	$⊢ φ \to \exists x \in (V ∖ \{\underset{˙}{0}\}) \underset{˙}{⊥} (L (G)) = N (\{x\})$

Metamath Proof Explorer

Theorem lcfl8b

Proof