Theorem lclkrlem2o

Description: Lemma for lclkr . When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B . (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	|- V = ( Base ` U )
	lclkrlem2m.t	|- .x. = ( .s ` U )
	lclkrlem2m.s	|- S = ( Scalar ` U )
	lclkrlem2m.q	|- .X. = ( .r ` S )
	lclkrlem2m.z	|- .0. = ( 0g ` S )
	lclkrlem2m.i	|- I = ( invr ` S )
	lclkrlem2m.m	|- .- = ( -g ` U )
	lclkrlem2m.f	|- F = ( LFnl ` U )
	lclkrlem2m.d	|- D = ( LDual ` U )
	lclkrlem2m.p	|- .+ = ( +g ` D )
	lclkrlem2m.x	|- ( ph -> X e. V )
	lclkrlem2m.y	|- ( ph -> Y e. V )
	lclkrlem2m.e	|- ( ph -> E e. F )
	lclkrlem2m.g	|- ( ph -> G e. F )
	lclkrlem2n.n	|- N = ( LSpan ` U )
	lclkrlem2n.l	|- L = ( LKer ` U )
	lclkrlem2o.h	|- H = ( LHyp ` K )
	lclkrlem2o.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lclkrlem2o.u	|- U = ( ( DVecH ` K ) ` W )
	lclkrlem2o.a	|- .(+) = ( LSSum ` U )
	lclkrlem2o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lclkrlem2o.b	|- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
	lclkrlem2o.n	|- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
	lclkrlem2o.bn	|- ( ph -> B =/= ( 0g ` U ) )
Assertion	lclkrlem2o	|- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	|- V = ( Base ` U )
2		lclkrlem2m.t	|- .x. = ( .s ` U )
3		lclkrlem2m.s	|- S = ( Scalar ` U )
4		lclkrlem2m.q	|- .X. = ( .r ` S )
5		lclkrlem2m.z	|- .0. = ( 0g ` S )
6		lclkrlem2m.i	|- I = ( invr ` S )
7		lclkrlem2m.m	|- .- = ( -g ` U )
8		lclkrlem2m.f	|- F = ( LFnl ` U )
9		lclkrlem2m.d	|- D = ( LDual ` U )
10		lclkrlem2m.p	|- .+ = ( +g ` D )
11		lclkrlem2m.x	|- ( ph -> X e. V )
12		lclkrlem2m.y	|- ( ph -> Y e. V )
13		lclkrlem2m.e	|- ( ph -> E e. F )
14		lclkrlem2m.g	|- ( ph -> G e. F )
15		lclkrlem2n.n	|- N = ( LSpan ` U )
16		lclkrlem2n.l	|- L = ( LKer ` U )
17		lclkrlem2o.h	|- H = ( LHyp ` K )
18		lclkrlem2o.o	|- ._|_ = ( ( ocH ` K ) ` W )
19		lclkrlem2o.u	|- U = ( ( DVecH ` K ) ` W )
20		lclkrlem2o.a	|- .(+) = ( LSSum ` U )
21		lclkrlem2o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
22		lclkrlem2o.b	|- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
23		lclkrlem2o.n	|- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
24		lclkrlem2o.bn	|- ( ph -> B =/= ( 0g ` U ) )
25		eqid	|- ( 0g ` U ) = ( 0g ` U )
26	17 19 21	dvhlvec	|- ( ph -> U e. LVec )
27	1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23	lclkrlem2m	|- ( ph -> ( B e. V /\ ( ( E .+ G ) ` B ) = .0. ) )
28	27	simpld	|- ( ph -> B e. V )
29		eldifsn	|- ( B e. ( V \ { ( 0g ` U ) } ) <-> ( B e. V /\ B =/= ( 0g ` U ) ) )
30	28 24 29	sylanbrc	|- ( ph -> B e. ( V \ { ( 0g ` U ) } ) )
31	17 18 19 1 25 21 30	dochnel	|- ( ph -> -. B e. ( ._|_ ` { B } ) )
32	17 19 21	dvhlmod	|- ( ph -> U e. LMod )
33	32	adantr	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> U e. LMod )
34	28	snssd	|- ( ph -> { B } C_ V )
35		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
36	17 19 1 35 18	dochlss	|- ( ( ( K e. HL /\ W e. H ) /\ { B } C_ V ) -> ( ._|_ ` { B } ) e. ( LSubSp ` U ) )
37	21 34 36	syl2anc	|- ( ph -> ( ._|_ ` { B } ) e. ( LSubSp ` U ) )
38	37	adantr	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> ( ._|_ ` { B } ) e. ( LSubSp ` U ) )
39		simprl	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> X e. ( ._|_ ` { B } ) )
40	3	lmodring	|- ( U e. LMod -> S e. Ring )
41	32 40	syl	|- ( ph -> S e. Ring )
42	8 9 10 32 13 14	ldualvaddcl	|- ( ph -> ( E .+ G ) e. F )
43		eqid	|- ( Base ` S ) = ( Base ` S )
44	3 43 1 8	lflcl	|- ( ( U e. LMod /\ ( E .+ G ) e. F /\ X e. V ) -> ( ( E .+ G ) ` X ) e. ( Base ` S ) )
45	32 42 11 44	syl3anc	|- ( ph -> ( ( E .+ G ) ` X ) e. ( Base ` S ) )
46	3	lvecdrng	|- ( U e. LVec -> S e. DivRing )
47	26 46	syl	|- ( ph -> S e. DivRing )
48	3 43 1 8	lflcl	|- ( ( U e. LMod /\ ( E .+ G ) e. F /\ Y e. V ) -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) )
49	32 42 12 48	syl3anc	|- ( ph -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) )
50	43 5 6	drnginvrcl	|- ( ( S e. DivRing /\ ( ( E .+ G ) ` Y ) e. ( Base ` S ) /\ ( ( E .+ G ) ` Y ) =/= .0. ) -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) )
51	47 49 23 50	syl3anc	|- ( ph -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) )
52	43 4	ringcl	|- ( ( S e. Ring /\ ( ( E .+ G ) ` X ) e. ( Base ` S ) /\ ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) ) -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) )
53	41 45 51 52	syl3anc	|- ( ph -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) )
54	53	adantr	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) )
55		simprr	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> Y e. ( ._|_ ` { B } ) )
56	3 2 43 35	lssvscl	|- ( ( ( U e. LMod /\ ( ._|_ ` { B } ) e. ( LSubSp ` U ) ) /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) /\ Y e. ( ._|_ ` { B } ) ) ) -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. ( ._|_ ` { B } ) )
57	33 38 54 55 56	syl22anc	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. ( ._|_ ` { B } ) )
58	7 35	lssvsubcl	|- ( ( ( U e. LMod /\ ( ._|_ ` { B } ) e. ( LSubSp ` U ) ) /\ ( X e. ( ._|_ ` { B } ) /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. ( ._|_ ` { B } ) ) ) -> ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) e. ( ._|_ ` { B } ) )
59	33 38 39 57 58	syl22anc	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) e. ( ._|_ ` { B } ) )
60	22 59	eqeltrid	|- ( ( ph /\ ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) ) -> B e. ( ._|_ ` { B } ) )
61	31 60	mtand	|- ( ph -> -. ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) )
62		ianor	|- ( -. ( X e. ( ._|_ ` { B } ) /\ Y e. ( ._|_ ` { B } ) ) <-> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
63	61 62	sylib	|- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )