dochkr1OLDN

Description: A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 . (Contributed by NM, 2-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dochkr1OLD.h	$⊢ H = LHyp (K)$
	dochkr1OLD.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochkr1OLD.u	$⊢ U = DVecH (K) (W)$
	dochkr1OLD.v	$⊢ V = {Base}_{U}$
	dochkr1OLD.r	$⊢ R = Scalar (U)$
	dochkr1OLD.z	$⊢ \underset{˙}{0} = 0_{R}$
	dochkr1OLD.i	$⊢ \underset{˙}{1} = 1_{R}$
	dochkr1OLD.f	$⊢ F = LFnl (U)$
	dochkr1OLD.l	$⊢ L = LKer (U)$
	dochkr1OLD.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochkr1OLD.g	$⊢ φ \to G \in F$
	dochkr1OLD.n	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V$
Assertion	dochkr1OLDN	$⊢ φ \to \exists x \in \underset{˙}{⊥} (L (G)) G (x) = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		dochkr1OLD.h	$⊢ H = LHyp (K)$
2		dochkr1OLD.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochkr1OLD.u	$⊢ U = DVecH (K) (W)$
4		dochkr1OLD.v	$⊢ V = {Base}_{U}$
5		dochkr1OLD.r	$⊢ R = Scalar (U)$
6		dochkr1OLD.z	$⊢ \underset{˙}{0} = 0_{R}$
7		dochkr1OLD.i	$⊢ \underset{˙}{1} = 1_{R}$
8		dochkr1OLD.f	$⊢ F = LFnl (U)$
9		dochkr1OLD.l	$⊢ L = LKer (U)$
10		dochkr1OLD.k	$⊢ φ \to (K \in HL \land W \in H)$
11		dochkr1OLD.g	$⊢ φ \to G \in F$
12		dochkr1OLD.n	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V$
13		eqid	$⊢ 0_{U} = 0_{U}$
14		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
15	1 3 10	dvhlmod	$⊢ φ \to U \in LMod$
16	1 2 3 4 14 8 9 10 11	dochkrsat2	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq V \leftrightarrow \underset{˙}{⊥} (L (G)) \in LSAtoms (U))$
17	12 16	mpbid	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in LSAtoms (U)$
18	13 14 15 17	lsateln0	$⊢ φ \to \exists z \in \underset{˙}{⊥} (L (G)) z \neq 0_{U}$
19	10	ad2antrr	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to (K \in HL \land W \in H)$
20	11	ad2antrr	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to G \in F$
21		eldifsn	$⊢ z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\}) \leftrightarrow (z \in \underset{˙}{⊥} (L (G)) \land z \neq 0_{U})$
22	21	biimpri	$⊢ (z \in \underset{˙}{⊥} (L (G)) \land z \neq 0_{U}) \to z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\})$
23	22	adantll	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\})$
24	1 2 3 4 5 6 13 8 9 19 20 23	dochfln0	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to G (z) \neq \underset{˙}{0}$
25	24	ex	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to (z \neq 0_{U} \to G (z) \neq \underset{˙}{0})$
26	25	reximdva	$⊢ φ \to (\exists z \in \underset{˙}{⊥} (L (G)) z \neq 0_{U} \to \exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq \underset{˙}{0})$
27	18 26	mpd	$⊢ φ \to \exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq \underset{˙}{0}$
28	4 8 9 15 11	lkrssv	$⊢ φ \to L (G) \subseteq V$
29		eqid	$⊢ LSubSp (U) = LSubSp (U)$
30	1 3 4 29 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq V) \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
31	10 28 30	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
32	15 31	jca	$⊢ φ \to (U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSubSp (U))$
33	32	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to (U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSubSp (U))$
34	1 3 10	dvhlvec	$⊢ φ \to U \in LVec$
35	34	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to U \in LVec$
36	5	lvecdrng	$⊢ U \in LVec \to R \in DivRing$
37	35 36	syl	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to R \in DivRing$
38	15	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to U \in LMod$
39	11	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to G \in F$
40	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq V) \to \underset{˙}{⊥} (L (G)) \subseteq V$
41	10 28 40	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \subseteq V$
42	41	sselda	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to z \in V$
43	42	3adant3	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to z \in V$
44		eqid	$⊢ {Base}_{R} = {Base}_{R}$
45	5 44 4 8	lflcl	$⊢ (U \in LMod \land G \in F \land z \in V) \to G (z) \in {Base}_{R}$
46	38 39 43 45	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to G (z) \in {Base}_{R}$
47		simp3	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to G (z) \neq \underset{˙}{0}$
48		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
49	44 6 48	drnginvrcl	$⊢ (R \in DivRing \land G (z) \in {Base}_{R} \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (R) (G (z)) \in {Base}_{R}$
50	37 46 47 49	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (R) (G (z)) \in {Base}_{R}$
51		simp2	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to z \in \underset{˙}{⊥} (L (G))$
52		eqid	$⊢ \cdot_{U} = \cdot_{U}$
53	5 52 44 29	lssvscl	$⊢ ((U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSubSp (U)) \land ({inv}_{r} (R) (G (z)) \in {Base}_{R} \land z \in \underset{˙}{⊥} (L (G)))) \to {inv}_{r} (R) (G (z)) \cdot_{U} z \in \underset{˙}{⊥} (L (G))$
54	33 50 51 53	syl12anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (R) (G (z)) \cdot_{U} z \in \underset{˙}{⊥} (L (G))$
55		eqid	$⊢ \cdot_{R} = \cdot_{R}$
56	5 44 55 4 52 8	lflmul	$⊢ (U \in LMod \land G \in F \land ({inv}_{r} (R) (G (z)) \in {Base}_{R} \land z \in V)) \to G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = {inv}_{r} (R) (G (z)) \cdot_{R} G (z)$
57	38 39 50 43 56	syl112anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = {inv}_{r} (R) (G (z)) \cdot_{R} G (z)$
58	44 6 55 7 48	drnginvrl	$⊢ (R \in DivRing \land G (z) \in {Base}_{R} \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (R) (G (z)) \cdot_{R} G (z) = \underset{˙}{1}$
59	37 46 47 58	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (R) (G (z)) \cdot_{R} G (z) = \underset{˙}{1}$
60	57 59	eqtrd	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = \underset{˙}{1}$
61		fveqeq2	$⊢ x = {inv}_{r} (R) (G (z)) \cdot_{U} z \to (G (x) = \underset{˙}{1} \leftrightarrow G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = \underset{˙}{1})$
62	61	rspcev	$⊢ ({inv}_{r} (R) (G (z)) \cdot_{U} z \in \underset{˙}{⊥} (L (G)) \land G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = \underset{˙}{1}) \to \exists x \in \underset{˙}{⊥} (L (G)) G (x) = \underset{˙}{1}$
63	54 60 62	syl2anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq \underset{˙}{0}) \to \exists x \in \underset{˙}{⊥} (L (G)) G (x) = \underset{˙}{1}$
64	63	rexlimdv3a	$⊢ φ \to (\exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq \underset{˙}{0} \to \exists x \in \underset{˙}{⊥} (L (G)) G (x) = \underset{˙}{1})$
65	27 64	mpd	$⊢ φ \to \exists x \in \underset{˙}{⊥} (L (G)) G (x) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem dochkr1OLDN

Proof