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 = Base U
lclkrlem2m.t · ˙ = U
lclkrlem2m.s S = Scalar U
lclkrlem2m.q × ˙ = S
lclkrlem2m.z 0 ˙ = 0 S
lclkrlem2m.i I = inv r S
lclkrlem2m.m - ˙ = - U
lclkrlem2m.f F = LFnl U
lclkrlem2m.d D = LDual U
lclkrlem2m.p + ˙ = + D
lclkrlem2m.x φ X V
lclkrlem2m.y φ Y V
lclkrlem2m.e φ E F
lclkrlem2m.g φ G 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 φ K HL W H
lclkrlem2o.b B = X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
lclkrlem2o.n φ E + ˙ G Y 0 ˙
lclkrlem2o.bn φ B 0 U
Assertion lclkrlem2o φ ¬ X ˙ B ¬ Y ˙ B

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v V = Base U
2 lclkrlem2m.t · ˙ = U
3 lclkrlem2m.s S = Scalar U
4 lclkrlem2m.q × ˙ = S
5 lclkrlem2m.z 0 ˙ = 0 S
6 lclkrlem2m.i I = inv r S
7 lclkrlem2m.m - ˙ = - U
8 lclkrlem2m.f F = LFnl U
9 lclkrlem2m.d D = LDual U
10 lclkrlem2m.p + ˙ = + D
11 lclkrlem2m.x φ X V
12 lclkrlem2m.y φ Y V
13 lclkrlem2m.e φ E F
14 lclkrlem2m.g φ G 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 φ K HL W H
22 lclkrlem2o.b B = X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
23 lclkrlem2o.n φ E + ˙ G Y 0 ˙
24 lclkrlem2o.bn φ B 0 U
25 eqid 0 U = 0 U
26 17 19 21 dvhlvec φ U LVec
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23 lclkrlem2m φ B V E + ˙ G B = 0 ˙
28 27 simpld φ B V
29 eldifsn B V 0 U B V B 0 U
30 28 24 29 sylanbrc φ B V 0 U
31 17 18 19 1 25 21 30 dochnel φ ¬ B ˙ B
32 17 19 21 dvhlmod φ U LMod
33 32 adantr φ X ˙ B Y ˙ B U LMod
34 28 snssd φ B V
35 eqid LSubSp U = LSubSp U
36 17 19 1 35 18 dochlss K HL W H B V ˙ B LSubSp U
37 21 34 36 syl2anc φ ˙ B LSubSp U
38 37 adantr φ X ˙ B Y ˙ B ˙ B LSubSp U
39 simprl φ X ˙ B Y ˙ B X ˙ B
40 3 lmodring U LMod S Ring
41 32 40 syl φ S Ring
42 8 9 10 32 13 14 ldualvaddcl φ E + ˙ G F
43 eqid Base S = Base S
44 3 43 1 8 lflcl U LMod E + ˙ G F X V E + ˙ G X Base S
45 32 42 11 44 syl3anc φ E + ˙ G X Base S
46 3 lvecdrng U LVec S DivRing
47 26 46 syl φ S DivRing
48 3 43 1 8 lflcl U LMod E + ˙ G F Y V E + ˙ G Y Base S
49 32 42 12 48 syl3anc φ E + ˙ G Y Base S
50 43 5 6 drnginvrcl S DivRing E + ˙ G Y Base S E + ˙ G Y 0 ˙ I E + ˙ G Y Base S
51 47 49 23 50 syl3anc φ I E + ˙ G Y Base S
52 43 4 ringcl S Ring E + ˙ G X Base S I E + ˙ G Y Base S E + ˙ G X × ˙ I E + ˙ G Y Base S
53 41 45 51 52 syl3anc φ E + ˙ G X × ˙ I E + ˙ G Y Base S
54 53 adantr φ X ˙ B Y ˙ B E + ˙ G X × ˙ I E + ˙ G Y Base S
55 simprr φ X ˙ B Y ˙ B Y ˙ B
56 3 2 43 35 lssvscl U LMod ˙ B LSubSp U E + ˙ G X × ˙ I E + ˙ G Y Base S Y ˙ B E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y ˙ B
57 33 38 54 55 56 syl22anc φ X ˙ B Y ˙ B E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y ˙ B
58 7 35 lssvsubcl U LMod ˙ B LSubSp U X ˙ B E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y ˙ B X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y ˙ B
59 33 38 39 57 58 syl22anc φ X ˙ B Y ˙ B X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y ˙ B
60 22 59 eqeltrid φ X ˙ B Y ˙ B B ˙ B
61 31 60 mtand φ ¬ X ˙ B Y ˙ B
62 ianor ¬ X ˙ B Y ˙ B ¬ X ˙ B ¬ Y ˙ B
63 61 62 sylib φ ¬ X ˙ B ¬ Y ˙ B