Metamath Proof Explorer


Theorem lclkrlem2t

Description: Lemma for lclkr . We eliminate all hypotheses with B here. (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
lclkrlem2t.n φ E + ˙ G Y 0 ˙
Assertion lclkrlem2t φ ˙ ˙ 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 lclkrlem2t.n φ E + ˙ G Y 0 ˙
25 11 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U X V
26 12 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U Y V
27 13 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U E F
28 14 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U G F
29 21 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U K HL W H
30 22 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U L E = ˙ X
31 23 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U L G = ˙ Y
32 eqid X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y
33 24 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U E + ˙ G Y 0 ˙
34 simpr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U
35 1 2 3 4 5 6 7 8 9 10 25 26 27 28 15 16 17 18 19 20 29 30 31 32 33 34 lclkrlem2s φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y = 0 U ˙ ˙ L E + ˙ G = L E + ˙ G
36 11 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U X V
37 12 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U Y V
38 13 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U E F
39 14 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U G F
40 21 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U K HL W H
41 22 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U L E = ˙ X
42 23 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U L G = ˙ Y
43 24 adantr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U E + ˙ G Y 0 ˙
44 simpr φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U
45 1 2 3 4 5 6 7 8 9 10 36 37 38 39 15 16 17 18 19 20 40 41 42 32 43 44 lclkrlem2q φ X - ˙ E + ˙ G X × ˙ I E + ˙ G Y · ˙ Y 0 U ˙ ˙ L E + ˙ G = L E + ˙ G
46 35 45 pm2.61dane φ ˙ ˙ L E + ˙ G = L E + ˙ G