lcfl8

Description: Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcfl8.h	$⊢ H = LHyp (K)$
2		lcfl8.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfl8.u	$⊢ U = DVecH (K) (W)$
4		lcfl8.v	$⊢ V = {Base}_{U}$
5		lcfl8.f	$⊢ F = LFnl (U)$
6		lcfl8.l	$⊢ L = LKer (U)$
7		lcfl8.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
8		lcfl8.k	$⊢ φ \to (K \in HL \land W \in H)$
9		lcfl8.g	$⊢ φ \to G \in F$
10	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
11	10	adantr	$⊢ (φ \land G \in C) \to U \in LMod$
12		eqid	$⊢ LSpan (U) = LSpan (U)$
13		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
14	4 12 13	islsati	$⊢ (U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \to \exists x \in V \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})$
15	11 14	sylan	$⊢ ((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \to \exists x \in V \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})$
16		simpr	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})$
17	16	fveq2d	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = \underset{˙}{⊥} (LSpan (U) (\{x\}))$
18		simp-4r	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to G \in C$
19	9	ad4antr	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to G \in F$
20	7 19	lcfl1	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to (G \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
21	18 20	mpbid	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
22	8	ad4antr	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to (K \in HL \land W \in H)$
23		simplr	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to x \in V$
24	23	snssd	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to \{x\} \subseteq V$
25	1 3 2 4 12 22 24	dochocsp	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to \underset{˙}{⊥} (LSpan (U) (\{x\})) = \underset{˙}{⊥} (\{x\})$
26	17 21 25	3eqtr3d	$⊢ ((((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \land \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\})) \to L (G) = \underset{˙}{⊥} (\{x\})$
27	26	ex	$⊢ (((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \land x \in V) \to (\underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\}) \to L (G) = \underset{˙}{⊥} (\{x\}))$
28	27	reximdva	$⊢ ((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \to (\exists x \in V \underset{˙}{⊥} (L (G)) = LSpan (U) (\{x\}) \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\}))$
29	15 28	mpd	$⊢ ((φ \land G \in C) \land \underset{˙}{⊥} (L (G)) \in LSAtoms (U)) \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\})$
30	11	adantr	$⊢ ((φ \land G \in C) \land L (G) = V) \to U \in LMod$
31		eqid	$⊢ 0_{U} = 0_{U}$
32	4 31	lmod0vcl	$⊢ U \in LMod \to 0_{U} \in V$
33	30 32	syl	$⊢ ((φ \land G \in C) \land L (G) = V) \to 0_{U} \in V$
34		simpr	$⊢ ((φ \land G \in C) \land L (G) = V) \to L (G) = V$
35	8	adantr	$⊢ (φ \land G \in C) \to (K \in HL \land W \in H)$
36	35	adantr	$⊢ ((φ \land G \in C) \land L (G) = V) \to (K \in HL \land W \in H)$
37	1 3 2 4 31	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{0_{U}\}) = V$
38	36 37	syl	$⊢ ((φ \land G \in C) \land L (G) = V) \to \underset{˙}{⊥} (\{0_{U}\}) = V$
39	34 38	eqtr4d	$⊢ ((φ \land G \in C) \land L (G) = V) \to L (G) = \underset{˙}{⊥} (\{0_{U}\})$
40		sneq	$⊢ x = 0_{U} \to \{x\} = \{0_{U}\}$
41	40	fveq2d	$⊢ x = 0_{U} \to \underset{˙}{⊥} (\{x\}) = \underset{˙}{⊥} (\{0_{U}\})$
42	41	rspceeqv	$⊢ (0_{U} \in V \land L (G) = \underset{˙}{⊥} (\{0_{U}\})) \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\})$
43	33 39 42	syl2anc	$⊢ ((φ \land G \in C) \land L (G) = V) \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\})$
44	1 2 3 4 13 5 6 7 8 9	lcfl3	$⊢ φ \to (G \in C \leftrightarrow (\underset{˙}{⊥} (L (G)) \in LSAtoms (U) \lor L (G) = V))$
45	44	biimpa	$⊢ (φ \land G \in C) \to (\underset{˙}{⊥} (L (G)) \in LSAtoms (U) \lor L (G) = V)$
46	29 43 45	mpjaodan	$⊢ (φ \land G \in C) \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\})$
47	46	ex	$⊢ φ \to (G \in C \to \exists x \in V L (G) = \underset{˙}{⊥} (\{x\}))$
48	8	3ad2ant1	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to (K \in HL \land W \in H)$
49		simp2	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to x \in V$
50	49	snssd	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \{x\} \subseteq V$
51		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
52	1 51 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{x\} \subseteq V) \to \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)$
53	48 50 52	syl2anc	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)$
54	1 51 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\{x\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))) = \underset{˙}{⊥} (\{x\})$
55	48 53 54	syl2anc	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))) = \underset{˙}{⊥} (\{x\})$
56		simp3	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to L (G) = \underset{˙}{⊥} (\{x\})$
57	56	fveq2d	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{x\}))$
58	57	fveq2d	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\{x\})))$
59	55 58 56	3eqtr4d	$⊢ (φ \land x \in V \land L (G) = \underset{˙}{⊥} (\{x\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
60	59	rexlimdv3a	$⊢ φ \to (\exists x \in V L (G) = \underset{˙}{⊥} (\{x\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
61	7 9	lcfl1	$⊢ φ \to (G \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
62	60 61	sylibrd	$⊢ φ \to (\exists x \in V L (G) = \underset{˙}{⊥} (\{x\}) \to G \in C)$
63	47 62	impbid	$⊢ φ \to (G \in C \leftrightarrow \exists x \in V L (G) = \underset{˙}{⊥} (\{x\}))$

Metamath Proof Explorer

Theorem lcfl8

Proof