dochkr1

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)

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

Proof

Step	Hyp	Ref	Expression
1		dochkr1.h	$⊢ H = LHyp (K)$
2		dochkr1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochkr1.u	$⊢ U = DVecH (K) (W)$
4		dochkr1.v	$⊢ V = {Base}_{U}$
5		dochkr1.r	$⊢ R = Scalar (U)$
6		dochkr1.z	$⊢ \underset{˙}{0} = 0_{U}$
7		dochkr1.i	$⊢ \underset{˙}{1} = 1_{R}$
8		dochkr1.f	$⊢ F = LFnl (U)$
9		dochkr1.l	$⊢ L = LKer (U)$
10		dochkr1.k	$⊢ φ \to (K \in HL \land W \in H)$
11		dochkr1.g	$⊢ φ \to G \in F$
12		dochkr1.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		eqid	$⊢ 0_{R} = 0_{R}$
20	10	ad2antrr	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to (K \in HL \land W \in H)$
21	11	ad2antrr	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to G \in F$
22		eldifsn	$⊢ z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\}) \leftrightarrow (z \in \underset{˙}{⊥} (L (G)) \land z \neq 0_{U})$
23	22	biimpri	$⊢ (z \in \underset{˙}{⊥} (L (G)) \land z \neq 0_{U}) \to z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\})$
24	23	adantll	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to z \in (\underset{˙}{⊥} (L (G)) ∖ \{0_{U}\})$
25	1 2 3 4 5 19 13 8 9 20 21 24	dochfln0	$⊢ ((φ \land z \in \underset{˙}{⊥} (L (G))) \land z \neq 0_{U}) \to G (z) \neq 0_{R}$
26	25	ex	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to (z \neq 0_{U} \to G (z) \neq 0_{R})$
27	26	reximdva	$⊢ φ \to (\exists z \in \underset{˙}{⊥} (L (G)) z \neq 0_{U} \to \exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq 0_{R})$
28	18 27	mpd	$⊢ φ \to \exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq 0_{R}$
29	4 8 9 15 11	lkrssv	$⊢ φ \to L (G) \subseteq V$
30		eqid	$⊢ LSubSp (U) = LSubSp (U)$
31	1 3 4 30 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq V) \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
32	10 29 31	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
33	15 32	jca	$⊢ φ \to (U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSubSp (U))$
34	33	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to (U \in LMod \land \underset{˙}{⊥} (L (G)) \in LSubSp (U))$
35	1 3 10	dvhlvec	$⊢ φ \to U \in LVec$
36	35	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to U \in LVec$
37	5	lvecdrng	$⊢ U \in LVec \to R \in DivRing$
38	36 37	syl	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to R \in DivRing$
39	15	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to U \in LMod$
40	11	3ad2ant1	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to G \in F$
41	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq V) \to \underset{˙}{⊥} (L (G)) \subseteq V$
42	10 29 41	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \subseteq V$
43	42	sselda	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to z \in V$
44	43	3adant3	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to z \in V$
45		eqid	$⊢ {Base}_{R} = {Base}_{R}$
46	5 45 4 8	lflcl	$⊢ (U \in LMod \land G \in F \land z \in V) \to G (z) \in {Base}_{R}$
47	39 40 44 46	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to G (z) \in {Base}_{R}$
48		simp3	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to G (z) \neq 0_{R}$
49		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
50	45 19 49	drnginvrcl	$⊢ (R \in DivRing \land G (z) \in {Base}_{R} \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \in {Base}_{R}$
51	38 47 48 50	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \in {Base}_{R}$
52		simp2	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to z \in \underset{˙}{⊥} (L (G))$
53	51 52	jca	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to ({inv}_{r} (R) (G (z)) \in {Base}_{R} \land z \in \underset{˙}{⊥} (L (G)))$
54		eqid	$⊢ \cdot_{U} = \cdot_{U}$
55	5 54 45 30	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))$
56	34 53 55	syl2anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \cdot_{U} z \in \underset{˙}{⊥} (L (G))$
57	45 19 49	drnginvrn0	$⊢ (R \in DivRing \land G (z) \in {Base}_{R} \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \neq 0_{R}$
58	38 47 48 57	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \neq 0_{R}$
59	15	adantr	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to U \in LMod$
60	11	adantr	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to G \in F$
61	5 19 6 8	lfl0	$⊢ (U \in LMod \land G \in F) \to G (\underset{˙}{0}) = 0_{R}$
62	59 60 61	syl2anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to G (\underset{˙}{0}) = 0_{R}$
63		fveqeq2	$⊢ z = \underset{˙}{0} \to (G (z) = 0_{R} \leftrightarrow G (\underset{˙}{0}) = 0_{R})$
64	62 63	syl5ibrcom	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to (z = \underset{˙}{0} \to G (z) = 0_{R})$
65	64	necon3d	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G))) \to (G (z) \neq 0_{R} \to z \neq \underset{˙}{0})$
66	65	3impia	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to z \neq \underset{˙}{0}$
67	4 54 5 45 19 6 36 51 44	lvecvsn0	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to ({inv}_{r} (R) (G (z)) \cdot_{U} z \neq \underset{˙}{0} \leftrightarrow ({inv}_{r} (R) (G (z)) \neq 0_{R} \land z \neq \underset{˙}{0}))$
68	58 66 67	mpbir2and	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \cdot_{U} z \neq \underset{˙}{0}$
69		eldifsn	$⊢ {inv}_{r} (R) (G (z)) \cdot_{U} z \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \leftrightarrow ({inv}_{r} (R) (G (z)) \cdot_{U} z \in \underset{˙}{⊥} (L (G)) \land {inv}_{r} (R) (G (z)) \cdot_{U} z \neq \underset{˙}{0})$
70	56 68 69	sylanbrc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \cdot_{U} z \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\})$
71		eqid	$⊢ \cdot_{R} = \cdot_{R}$
72	5 45 71 4 54 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)$
73	39 40 51 44 72	syl112anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = {inv}_{r} (R) (G (z)) \cdot_{R} G (z)$
74	45 19 71 7 49	drnginvrl	$⊢ (R \in DivRing \land G (z) \in {Base}_{R} \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \cdot_{R} G (z) = \underset{˙}{1}$
75	38 47 48 74	syl3anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to {inv}_{r} (R) (G (z)) \cdot_{R} G (z) = \underset{˙}{1}$
76	73 75	eqtrd	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = \underset{˙}{1}$
77		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})$
78	77	rspcev	$⊢ ({inv}_{r} (R) (G (z)) \cdot_{U} z \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \land G ({inv}_{r} (R) (G (z)) \cdot_{U} z) = \underset{˙}{1}) \to \exists x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) G (x) = \underset{˙}{1}$
79	70 76 78	syl2anc	$⊢ (φ \land z \in \underset{˙}{⊥} (L (G)) \land G (z) \neq 0_{R}) \to \exists x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) G (x) = \underset{˙}{1}$
80	79	rexlimdv3a	$⊢ φ \to (\exists z \in \underset{˙}{⊥} (L (G)) G (z) \neq 0_{R} \to \exists x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) G (x) = \underset{˙}{1})$
81	28 80	mpd	$⊢ φ \to \exists x \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) G (x) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem dochkr1

Proof