Metamath Proof Explorer


Theorem lclkrlem2i

Description: Lemma for lclkr . Eliminate the ( LE ) =/= ( LG ) hypothesis. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2f.h H = LHyp K
lclkrlem2f.o ˙ = ocH K W
lclkrlem2f.u U = DVecH K W
lclkrlem2f.v V = Base U
lclkrlem2f.s S = Scalar U
lclkrlem2f.q Q = 0 S
lclkrlem2f.z 0 ˙ = 0 U
lclkrlem2f.a ˙ = LSSum U
lclkrlem2f.n N = LSpan U
lclkrlem2f.f F = LFnl U
lclkrlem2f.j J = LSHyp U
lclkrlem2f.l L = LKer U
lclkrlem2f.d D = LDual U
lclkrlem2f.p + ˙ = + D
lclkrlem2f.k φ K HL W H
lclkrlem2f.b φ B V 0 ˙
lclkrlem2f.e φ E F
lclkrlem2f.g φ G F
lclkrlem2f.le φ L E = ˙ X
lclkrlem2f.lg φ L G = ˙ Y
lclkrlem2f.kb φ E + ˙ G B = Q
lclkrlem2f.nx φ ¬ X ˙ B ¬ Y ˙ B
lclkrlem2i.x φ X V 0 ˙
lclkrlem2i.y φ Y V 0 ˙
Assertion lclkrlem2i φ ˙ ˙ L E + ˙ G = L E + ˙ G

Proof

Step Hyp Ref Expression
1 lclkrlem2f.h H = LHyp K
2 lclkrlem2f.o ˙ = ocH K W
3 lclkrlem2f.u U = DVecH K W
4 lclkrlem2f.v V = Base U
5 lclkrlem2f.s S = Scalar U
6 lclkrlem2f.q Q = 0 S
7 lclkrlem2f.z 0 ˙ = 0 U
8 lclkrlem2f.a ˙ = LSSum U
9 lclkrlem2f.n N = LSpan U
10 lclkrlem2f.f F = LFnl U
11 lclkrlem2f.j J = LSHyp U
12 lclkrlem2f.l L = LKer U
13 lclkrlem2f.d D = LDual U
14 lclkrlem2f.p + ˙ = + D
15 lclkrlem2f.k φ K HL W H
16 lclkrlem2f.b φ B V 0 ˙
17 lclkrlem2f.e φ E F
18 lclkrlem2f.g φ G F
19 lclkrlem2f.le φ L E = ˙ X
20 lclkrlem2f.lg φ L G = ˙ Y
21 lclkrlem2f.kb φ E + ˙ G B = Q
22 lclkrlem2f.nx φ ¬ X ˙ B ¬ Y ˙ B
23 lclkrlem2i.x φ X V 0 ˙
24 lclkrlem2i.y φ Y V 0 ˙
25 15 adantr φ L E = L G K HL W H
26 23 adantr φ L E = L G X V 0 ˙
27 17 adantr φ L E = L G E F
28 18 adantr φ L E = L G G F
29 19 adantr φ L E = L G L E = ˙ X
30 simpr φ L E = L G L E = L G
31 1 2 3 4 7 10 12 13 14 25 26 27 28 29 30 lclkrlem2e φ L E = L G ˙ ˙ L E + ˙ G = L E + ˙ G
32 15 adantr φ L E L G K HL W H
33 16 adantr φ L E L G B V 0 ˙
34 17 adantr φ L E L G E F
35 18 adantr φ L E L G G F
36 19 adantr φ L E L G L E = ˙ X
37 20 adantr φ L E L G L G = ˙ Y
38 21 adantr φ L E L G E + ˙ G B = Q
39 22 adantr φ L E L G ¬ X ˙ B ¬ Y ˙ B
40 23 adantr φ L E L G X V 0 ˙
41 24 adantr φ L E L G Y V 0 ˙
42 simpr φ L E L G L E L G
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 33 34 35 36 37 38 39 40 41 42 lclkrlem2h φ L E L G ˙ ˙ L E + ˙ G = L E + ˙ G
44 31 43 pm2.61dane φ ˙ ˙ L E + ˙ G = L E + ˙ G