Metamath Proof Explorer


Theorem lclkrlem2k

Description: Lemma for lclkr . Kernel closure when X is zero. (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
lclkrlem2k.x φ X = 0 ˙
lclkrlem2k.y φ Y V
Assertion lclkrlem2k φ ˙ ˙ 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 lclkrlem2k.x φ X = 0 ˙
24 lclkrlem2k.y φ Y V
25 1 3 15 dvhlmod φ U LMod
26 10 13 14 25 17 18 ldualvaddcom φ E + ˙ G = G + ˙ E
27 26 fveq1d φ E + ˙ G B = G + ˙ E B
28 27 21 eqtr3d φ G + ˙ E B = Q
29 22 orcomd φ ¬ Y ˙ B ¬ X ˙ B
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 18 17 20 19 28 29 24 23 lclkrlem2j φ ˙ ˙ L G + ˙ E = L G + ˙ E
31 26 fveq2d φ L E + ˙ G = L G + ˙ E
32 31 fveq2d φ ˙ L E + ˙ G = ˙ L G + ˙ E
33 32 fveq2d φ ˙ ˙ L E + ˙ G = ˙ ˙ L G + ˙ E
34 30 33 31 3eqtr4d φ ˙ ˙ L E + ˙ G = L E + ˙ G