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	|- H = ( LHyp ` K )
	dochkr1OLD.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochkr1OLD.u	|- U = ( ( DVecH ` K ) ` W )
	dochkr1OLD.v	|- V = ( Base ` U )
	dochkr1OLD.r	|- R = ( Scalar ` U )
	dochkr1OLD.z	|- .0. = ( 0g ` R )
	dochkr1OLD.i	|- .1. = ( 1r ` R )
	dochkr1OLD.f	|- F = ( LFnl ` U )
	dochkr1OLD.l	|- L = ( LKer ` U )
	dochkr1OLD.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochkr1OLD.g	|- ( ph -> G e. F )
	dochkr1OLD.n	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
Assertion	dochkr1OLDN	|- ( ph -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. )

Proof

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