lcfl6

Description: Property of a functional with a closed kernel. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 3-Jan-2015)

	Ref	Expression
Hypotheses	lcfl6.h	$⊢ H = LHyp (K)$
	lcfl6.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfl6.u	$⊢ U = DVecH (K) (W)$
	lcfl6.v	$⊢ V = {Base}_{U}$
	lcfl6.a	$⊢ \underset{˙}{+} = +_{U}$
	lcfl6.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfl6.s	$⊢ S = Scalar (U)$
	lcfl6.r	$⊢ R = {Base}_{S}$
	lcfl6.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfl6.f	$⊢ F = LFnl (U)$
	lcfl6.l	$⊢ L = LKer (U)$
	lcfl6.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfl6.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfl6.g	$⊢ φ \to G \in F$
Assertion	lcfl6	$⊢ φ \to (G \in C \leftrightarrow (L (G) = V \lor \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))))$

Proof

Step	Hyp	Ref	Expression
1		lcfl6.h	$⊢ H = LHyp (K)$
2		lcfl6.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfl6.u	$⊢ U = DVecH (K) (W)$
4		lcfl6.v	$⊢ V = {Base}_{U}$
5		lcfl6.a	$⊢ \underset{˙}{+} = +_{U}$
6		lcfl6.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		lcfl6.s	$⊢ S = Scalar (U)$
8		lcfl6.r	$⊢ R = {Base}_{S}$
9		lcfl6.z	$⊢ \underset{˙}{0} = 0_{U}$
10		lcfl6.f	$⊢ F = LFnl (U)$
11		lcfl6.l	$⊢ L = LKer (U)$
12		lcfl6.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
13		lcfl6.k	$⊢ φ \to (K \in HL \land W \in H)$
14		lcfl6.g	$⊢ φ \to G \in F$
15		df-ne	$⊢ L (G) \neq V \leftrightarrow \neg L (G) = V$
16		eqid	$⊢ 1_{S} = 1_{S}$
17	13	ad2antrr	$⊢ ((φ \land G \in C) \land L (G) \neq V) \to (K \in HL \land W \in H)$
18	14	ad2antrr	$⊢ ((φ \land G \in C) \land L (G) \neq V) \to G \in F$
19	1 2 3 4 10 11 12 13 14	lcfl2	$⊢ φ \to (G \in C \leftrightarrow (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V \lor L (G) = V))$
20	19	biimpa	$⊢ (φ \land G \in C) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V \lor L (G) = V)$
21	20	orcomd	$⊢ (φ \land G \in C) \to (L (G) = V \lor \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V)$
22	21	ord	$⊢ (φ \land G \in C) \to (\neg L (G) = V \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V)$
23	15 22	biimtrid	$⊢ (φ \land G \in C) \to (L (G) \neq V \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V)$
24	23	imp	$⊢ ((φ \land G \in C) \land L (G) \neq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V$
25	1 2 3 4 7 9 16 10 11 17 18 24	dochkr1	$⊢ ((φ \land G \in C) \land L (G) \neq V) \to \exists x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) G (x) = 1_{S}$
26	1 3 13	dvhlmod	$⊢ φ \to U \in LMod$
27	4 10 11 26 14	lkrssv	$⊢ φ \to L (G) \subseteq V$
28	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq V) \to \underset{˙}{⊥} (L (G)) \subseteq V$
29	13 27 28	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \subseteq V$
30	29	ssdifd	$⊢ φ \to \underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
31	30	ad3antrrr	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to \underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
32		simprl	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\})$
33	31 32	sseldd	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to x \in (V ∖ \{\underset{˙}{0}\})$
34	13	ad3antrrr	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to (K \in HL \land W \in H)$
35	14	ad3antrrr	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to G \in F$
36		simprr	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to G (x) = 1_{S}$
37	1 2 3 4 5 6 7 16 8 9 10 11 34 35 32 36	lcfl6lem	$⊢ (((φ \land G \in C) \land L (G) \neq V) \land (x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G (x) = 1_{S})) \to G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))$
38	25 33 37	reximssdv	$⊢ ((φ \land G \in C) \land L (G) \neq V) \to \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))$
39	38	ex	$⊢ (φ \land G \in C) \to (L (G) \neq V \to \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
40	15 39	biimtrrid	$⊢ (φ \land G \in C) \to (\neg L (G) = V \to \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
41	40	orrd	$⊢ (φ \land G \in C) \to (L (G) = V \lor \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
42	41	ex	$⊢ φ \to (G \in C \to (L (G) = V \lor \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))))$
43		olc	$⊢ L (G) = V \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V \lor L (G) = V)$
44	43 19	imbitrrid	$⊢ φ \to (L (G) = V \to G \in C)$
45	13	adantr	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to (K \in HL \land W \in H)$
46		eldifi	$⊢ x \in (V ∖ \{\underset{˙}{0}\}) \to x \in V$
47	46	adantl	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to x \in V$
48	47	snssd	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to \{x\} \subseteq V$
49		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
50	1 49 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{x\} \subseteq V) \to \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)$
51	45 48 50	syl2anc	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)$
52	1 49 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))) = \underset{˙}{⊥} (\{x\})$
53	45 51 52	syl2anc	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))) = \underset{˙}{⊥} (\{x\})$
54	53	3adant3	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))) = \underset{˙}{⊥} (\{x\})$
55		simp3	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))$
56	55	fveq2d	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to L (G) = L ((v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
57		eqid	$⊢ (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))) = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))$
58		simpr	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to x \in (V ∖ \{\underset{˙}{0}\})$
59	1 2 3 4 9 5 6 11 7 8 57 45 58	dochsnkr2	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to L ((v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) = \underset{˙}{⊥} (\{x\})$
60	59	3adant3	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to L ((v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) = \underset{˙}{⊥} (\{x\})$
61	56 60	eqtrd	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to L (G) = \underset{˙}{⊥} (\{x\})$
62	61	fveq2d	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))$
63	62	fveq2d	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\})))$
64	54 63 61	3eqtr4d	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
65	14	3ad2ant1	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to G \in F$
66	12 65	lcfl1	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to (G \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
67	64 66	mpbird	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\}) \land G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to G \in C$
68	67	rexlimdv3a	$⊢ φ \to (\exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))) \to G \in C)$
69	44 68	jaod	$⊢ φ \to ((L (G) = V \lor \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))) \to G \in C)$
70	42 69	impbid	$⊢ φ \to (G \in C \leftrightarrow (L (G) = V \lor \exists x \in (V ∖ \{\underset{˙}{0}\}) G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x)))))$

Metamath Proof Explorer

Theorem lcfl6

Proof