Metamath Proof Explorer


Theorem lclkrlem2p

Description: Lemma for lclkr . When B is zero, X and Y must colinear, so their orthocomplements must be comparable. (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 ˙
lclkrlem2p.bn φ B = 0 U
Assertion lclkrlem2p φ ˙ Y ˙ X

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 lclkrlem2p.bn φ B = 0 U
25 17 19 21 dvhlmod φ U LMod
26 eqid LSubSp U = LSubSp U
27 1 26 15 lspsncl U LMod Y V N Y LSubSp U
28 25 12 27 syl2anc φ N Y LSubSp U
29 1 26 lssss N Y LSubSp U N Y V
30 28 29 syl φ N Y V
31 22 24 eqtr3id φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U
32 3 lmodring U LMod S Ring
33 25 32 syl φ S Ring
34 8 9 10 25 13 14 ldualvaddcl φ E + ˙ G F
35 eqid Base S = Base S
36 3 35 1 8 lflcl U LMod E + ˙ G F X V E + ˙ G X Base S
37 25 34 11 36 syl3anc φ E + ˙ G X Base S
38 17 19 21 dvhlvec φ U LVec
39 3 lvecdrng U LVec S DivRing
40 38 39 syl φ S DivRing
41 3 35 1 8 lflcl U LMod E + ˙ G F Y V E + ˙ G Y Base S
42 25 34 12 41 syl3anc φ E + ˙ G Y Base S
43 35 5 6 drnginvrcl S DivRing E + ˙ G Y Base S E + ˙ G Y 0 ˙ I E + ˙ G Y Base S
44 40 42 23 43 syl3anc φ I E + ˙ G Y Base S
45 35 4 ringcl S Ring E + ˙ G X Base S I E + ˙ G Y Base S E + ˙ G X × ˙ I E + ˙ G Y Base S
46 33 37 44 45 syl3anc φ E + ˙ G X × ˙ I E + ˙ G Y Base S
47 1 3 2 35 lmodvscl U LMod E + ˙ G X × ˙ I E + ˙ G Y Base S Y V E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y V
48 25 46 12 47 syl3anc φ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y V
49 eqid 0 U = 0 U
50 1 49 7 lmodsubeq0 U LMod X V E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y V X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U X = E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
51 25 11 48 50 syl3anc φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U X = E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
52 31 51 mpbid φ X = E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
53 52 sneqd φ X = E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
54 53 fveq2d φ N X = N E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
55 3 35 1 2 15 lspsnvsi U LMod E + ˙ G X × ˙ I E + ˙ G Y Base S Y V N E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y N Y
56 25 46 12 55 syl3anc φ N E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y N Y
57 54 56 eqsstrd φ N X N Y
58 17 19 1 18 dochss K HL W H N Y V N X N Y ˙ N Y ˙ N X
59 21 30 57 58 syl3anc φ ˙ N Y ˙ N X
60 12 snssd φ Y V
61 17 19 18 1 15 21 60 dochocsp φ ˙ N Y = ˙ Y
62 11 snssd φ X V
63 17 19 18 1 15 21 62 dochocsp φ ˙ N X = ˙ X
64 59 61 63 3sstr3d φ ˙ Y ˙ X