Metamath Proof Explorer


Theorem lclkrlem2q

Description: Lemma for lclkr . The sum has a closed kernel when B is nonzero. (Contributed by NM, 18-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
lclkrlem2q.le φ L E = ˙ X
lclkrlem2q.lg φ L G = ˙ Y
lclkrlem2q.b B = X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
lclkrlem2q.n φ E + ˙ G Y 0 ˙
lclkrlem2q.bn φ B 0 U
Assertion lclkrlem2q φ ˙ ˙ L E + ˙ G = L E + ˙ G

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 lclkrlem2q.le φ L E = ˙ X
23 lclkrlem2q.lg φ L G = ˙ Y
24 lclkrlem2q.b B = X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
25 lclkrlem2q.n φ E + ˙ G Y 0 ˙
26 lclkrlem2q.bn φ B 0 U
27 eqid 0 U = 0 U
28 eqid LSHyp U = LSHyp U
29 17 19 21 dvhlvec φ U LVec
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 29 24 25 lclkrlem2m φ B V E + ˙ G B = 0 ˙
31 30 simpld φ B V
32 eldifsn B V 0 U B V B 0 U
33 31 26 32 sylanbrc φ B V 0 U
34 30 simprd φ E + ˙ G B = 0 ˙
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 24 25 26 lclkrlem2o φ ¬ X ˙ B ¬ Y ˙ B
36 17 18 19 1 3 5 27 20 15 8 28 16 9 10 21 33 13 14 22 23 34 35 11 12 lclkrlem2l φ ˙ ˙ L E + ˙ G = L E + ˙ G