Metamath Proof Explorer


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=BaseU
lclkrlem2m.t ·˙=U
lclkrlem2m.s S=ScalarU
lclkrlem2m.q ×˙=S
lclkrlem2m.z 0˙=0S
lclkrlem2m.i I=invrS
lclkrlem2m.m -˙=-U
lclkrlem2m.f F=LFnlU
lclkrlem2m.d D=LDualU
lclkrlem2m.p +˙=+D
lclkrlem2m.x φXV
lclkrlem2m.y φYV
lclkrlem2m.e φEF
lclkrlem2m.g φGF
lclkrlem2n.n N=LSpanU
lclkrlem2n.l L=LKerU
lclkrlem2o.h H=LHypK
lclkrlem2o.o ˙=ocHKW
lclkrlem2o.u U=DVecHKW
lclkrlem2o.a ˙=LSSumU
lclkrlem2o.k φKHLWH
lclkrlem2o.b B=X-˙E+˙GX×˙IE+˙GY·˙Y
lclkrlem2o.n φE+˙GY0˙
lclkrlem2o.bn φB0U
Assertion lclkrlem2o φ¬X˙B¬Y˙B

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v V=BaseU
2 lclkrlem2m.t ·˙=U
3 lclkrlem2m.s S=ScalarU
4 lclkrlem2m.q ×˙=S
5 lclkrlem2m.z 0˙=0S
6 lclkrlem2m.i I=invrS
7 lclkrlem2m.m -˙=-U
8 lclkrlem2m.f F=LFnlU
9 lclkrlem2m.d D=LDualU
10 lclkrlem2m.p +˙=+D
11 lclkrlem2m.x φXV
12 lclkrlem2m.y φYV
13 lclkrlem2m.e φEF
14 lclkrlem2m.g φGF
15 lclkrlem2n.n N=LSpanU
16 lclkrlem2n.l L=LKerU
17 lclkrlem2o.h H=LHypK
18 lclkrlem2o.o ˙=ocHKW
19 lclkrlem2o.u U=DVecHKW
20 lclkrlem2o.a ˙=LSSumU
21 lclkrlem2o.k φKHLWH
22 lclkrlem2o.b B=X-˙E+˙GX×˙IE+˙GY·˙Y
23 lclkrlem2o.n φE+˙GY0˙
24 lclkrlem2o.bn φB0U
25 eqid 0U=0U
26 17 19 21 dvhlvec φULVec
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23 lclkrlem2m φBVE+˙GB=0˙
28 27 simpld φBV
29 eldifsn BV0UBVB0U
30 28 24 29 sylanbrc φBV0U
31 17 18 19 1 25 21 30 dochnel φ¬B˙B
32 17 19 21 dvhlmod φULMod
33 32 adantr φX˙BY˙BULMod
34 28 snssd φBV
35 eqid LSubSpU=LSubSpU
36 17 19 1 35 18 dochlss KHLWHBV˙BLSubSpU
37 21 34 36 syl2anc φ˙BLSubSpU
38 37 adantr φX˙BY˙B˙BLSubSpU
39 simprl φX˙BY˙BX˙B
40 3 lmodring ULModSRing
41 32 40 syl φSRing
42 8 9 10 32 13 14 ldualvaddcl φE+˙GF
43 eqid BaseS=BaseS
44 3 43 1 8 lflcl ULModE+˙GFXVE+˙GXBaseS
45 32 42 11 44 syl3anc φE+˙GXBaseS
46 3 lvecdrng ULVecSDivRing
47 26 46 syl φSDivRing
48 3 43 1 8 lflcl ULModE+˙GFYVE+˙GYBaseS
49 32 42 12 48 syl3anc φE+˙GYBaseS
50 43 5 6 drnginvrcl SDivRingE+˙GYBaseSE+˙GY0˙IE+˙GYBaseS
51 47 49 23 50 syl3anc φIE+˙GYBaseS
52 43 4 ringcl SRingE+˙GXBaseSIE+˙GYBaseSE+˙GX×˙IE+˙GYBaseS
53 41 45 51 52 syl3anc φE+˙GX×˙IE+˙GYBaseS
54 53 adantr φX˙BY˙BE+˙GX×˙IE+˙GYBaseS
55 simprr φX˙BY˙BY˙B
56 3 2 43 35 lssvscl ULMod˙BLSubSpUE+˙GX×˙IE+˙GYBaseSY˙BE+˙GX×˙IE+˙GY·˙Y˙B
57 33 38 54 55 56 syl22anc φX˙BY˙BE+˙GX×˙IE+˙GY·˙Y˙B
58 7 35 lssvsubcl ULMod˙BLSubSpUX˙BE+˙GX×˙IE+˙GY·˙Y˙BX-˙E+˙GX×˙IE+˙GY·˙Y˙B
59 33 38 39 57 58 syl22anc φX˙BY˙BX-˙E+˙GX×˙IE+˙GY·˙Y˙B
60 22 59 eqeltrid φX˙BY˙BB˙B
61 31 60 mtand φ¬X˙BY˙B
62 ianor ¬X˙BY˙B¬X˙B¬Y˙B
63 61 62 sylib φ¬X˙B¬Y˙B