Theorem 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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochkr1OLD.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochkr1OLD.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochkr1OLD.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochkr1OLD.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	dochkr1OLD.z	⊢ 0 = ( 0g ‘ 𝑅 )
	dochkr1OLD.i	⊢ 1 = ( 1r ‘ 𝑅 )
	dochkr1OLD.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	dochkr1OLD.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	dochkr1OLD.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochkr1OLD.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	dochkr1OLD.n	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
Assertion	dochkr1OLDN	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		dochkr1OLD.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochkr1OLD.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochkr1OLD.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochkr1OLD.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochkr1OLD.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		dochkr1OLD.z	⊢ 0 = ( 0g ‘ 𝑅 )
7		dochkr1OLD.i	⊢ 1 = ( 1r ‘ 𝑅 )
8		dochkr1OLD.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9		dochkr1OLD.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
10		dochkr1OLD.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		dochkr1OLD.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
12		dochkr1OLD.n	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
13		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
14		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
15	1 3 10	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
16	1 2 3 4 14 8 9 10 11	dochkrsat2	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) )
17	12 16	mpbid	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
18	13 14 15 17	lsateln0	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) )
19	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝐺 ∈ 𝐹 )
21		eldifsn	⊢ ( 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) )
22	21	biimpri	⊢ ( ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
23	22	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
24	1 2 3 4 5 6 13 8 9 19 20 23	dochfln0	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
25	24	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( 𝑧 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
26	25	reximdva	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
27	18 26	mpd	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 )
28	4 8 9 15 11	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
29		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
30	1 3 4 29 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
31	10 28 30	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
32	15 31	jca	⊢ ( 𝜑 → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
33	32	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
34	1 3 10	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
35	34	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑈 ∈ LVec )
36	5	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
37	35 36	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑅 ∈ DivRing )
38	15	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑈 ∈ LMod )
39	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐺 ∈ 𝐹 )
40	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
41	10 28 40	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
42	41	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → 𝑧 ∈ 𝑉 )
43	42	3adant3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ 𝑉 )
44		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
45	5 44 4 8	lflcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
46	38 39 43 45	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
47		simp3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
48		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
49	44 6 48	drnginvrcl	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
50	37 46 47 49	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
51		simp2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
52		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
53	5 52 44 29	lssvscl	⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
54	33 50 51 53	syl12anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
55		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
56	5 44 55 4 52 8	lflmul	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
57	38 39 50 43 56	syl112anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
58	44 6 55 7 48	drnginvrl	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
59	37 46 47 58	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
60	57 59	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 )
61		fveqeq2	⊢ ( 𝑥 = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) = 1 ↔ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) )
62	61	rspcev	⊢ ( ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )
63	54 60 62	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )
64	63	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 ) )
65	27 64	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )