Metamath Proof Explorer


Theorem lclkrlem2l

Description: Lemma for lclkr . Eliminate the X =/= .0. , Y =/= .0. hypotheses. (Contributed by NM, 18-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
lclkrlem2l.x φ X V
lclkrlem2l.y φ Y V
Assertion lclkrlem2l φ ˙ ˙ 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 lclkrlem2l.x φ X V
24 lclkrlem2l.y φ Y V
25 15 adantr φ X = 0 ˙ K HL W H
26 16 adantr φ X = 0 ˙ B V 0 ˙
27 17 adantr φ X = 0 ˙ E F
28 18 adantr φ X = 0 ˙ G F
29 19 adantr φ X = 0 ˙ L E = ˙ X
30 20 adantr φ X = 0 ˙ L G = ˙ Y
31 21 adantr φ X = 0 ˙ E + ˙ G B = Q
32 22 adantr φ X = 0 ˙ ¬ X ˙ B ¬ Y ˙ B
33 simpr φ X = 0 ˙ X = 0 ˙
34 24 adantr φ X = 0 ˙ Y V
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 25 26 27 28 29 30 31 32 33 34 lclkrlem2k φ X = 0 ˙ ˙ ˙ L E + ˙ G = L E + ˙ G
36 15 adantr φ Y = 0 ˙ K HL W H
37 16 adantr φ Y = 0 ˙ B V 0 ˙
38 17 adantr φ Y = 0 ˙ E F
39 18 adantr φ Y = 0 ˙ G F
40 19 adantr φ Y = 0 ˙ L E = ˙ X
41 20 adantr φ Y = 0 ˙ L G = ˙ Y
42 21 adantr φ Y = 0 ˙ E + ˙ G B = Q
43 22 adantr φ Y = 0 ˙ ¬ X ˙ B ¬ Y ˙ B
44 23 adantr φ Y = 0 ˙ X V
45 simpr φ Y = 0 ˙ Y = 0 ˙
46 1 2 3 4 5 6 7 8 9 10 11 12 13 14 36 37 38 39 40 41 42 43 44 45 lclkrlem2j φ Y = 0 ˙ ˙ ˙ L E + ˙ G = L E + ˙ G
47 15 adantr φ X 0 ˙ Y 0 ˙ K HL W H
48 16 adantr φ X 0 ˙ Y 0 ˙ B V 0 ˙
49 17 adantr φ X 0 ˙ Y 0 ˙ E F
50 18 adantr φ X 0 ˙ Y 0 ˙ G F
51 19 adantr φ X 0 ˙ Y 0 ˙ L E = ˙ X
52 20 adantr φ X 0 ˙ Y 0 ˙ L G = ˙ Y
53 21 adantr φ X 0 ˙ Y 0 ˙ E + ˙ G B = Q
54 22 adantr φ X 0 ˙ Y 0 ˙ ¬ X ˙ B ¬ Y ˙ B
55 23 adantr φ X 0 ˙ Y 0 ˙ X V
56 simprl φ X 0 ˙ Y 0 ˙ X 0 ˙
57 eldifsn X V 0 ˙ X V X 0 ˙
58 55 56 57 sylanbrc φ X 0 ˙ Y 0 ˙ X V 0 ˙
59 24 adantr φ X 0 ˙ Y 0 ˙ Y V
60 simprr φ X 0 ˙ Y 0 ˙ Y 0 ˙
61 eldifsn Y V 0 ˙ Y V Y 0 ˙
62 59 60 61 sylanbrc φ X 0 ˙ Y 0 ˙ Y V 0 ˙
63 1 2 3 4 5 6 7 8 9 10 11 12 13 14 47 48 49 50 51 52 53 54 58 62 lclkrlem2i φ X 0 ˙ Y 0 ˙ ˙ ˙ L E + ˙ G = L E + ˙ G
64 35 46 63 pm2.61da2ne φ ˙ ˙ L E + ˙ G = L E + ˙ G