Metamath Proof Explorer


Theorem lclkrlem2s

Description: Lemma for lclkr . Thus, the sum has a closed kernel when B is zero. (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 ˙
lclkrlem2r.bn φ B = 0 U
Assertion lclkrlem2s φ ˙ ˙ 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 lclkrlem2r.bn φ B = 0 U
27 12 snssd φ Y V
28 eqid DIsoH K W = DIsoH K W
29 17 28 19 1 18 dochcl K HL W H Y V ˙ Y ran DIsoH K W
30 21 27 29 syl2anc φ ˙ Y ran DIsoH K W
31 17 28 18 dochoc K HL W H ˙ Y ran DIsoH K W ˙ ˙ ˙ Y = ˙ Y
32 21 30 31 syl2anc φ ˙ ˙ ˙ Y = ˙ Y
33 32 ad2antrr φ L G LSHyp U L E + ˙ G LSHyp U ˙ ˙ ˙ Y = ˙ Y
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 lclkrlem2r φ L G L E + ˙ G
35 34 ad2antrr φ L G LSHyp U L E + ˙ G LSHyp U L G L E + ˙ G
36 eqid LSHyp U = LSHyp U
37 17 19 21 dvhlvec φ U LVec
38 37 ad2antrr φ L G LSHyp U L E + ˙ G LSHyp U U LVec
39 simplr φ L G LSHyp U L E + ˙ G LSHyp U L G LSHyp U
40 simpr φ L G LSHyp U L E + ˙ G LSHyp U L E + ˙ G LSHyp U
41 36 38 39 40 lshpcmp φ L G LSHyp U L E + ˙ G LSHyp U L G L E + ˙ G L G = L E + ˙ G
42 35 41 mpbid φ L G LSHyp U L E + ˙ G LSHyp U L G = L E + ˙ G
43 23 ad2antrr φ L G LSHyp U L E + ˙ G LSHyp U L G = ˙ Y
44 42 43 eqtr3d φ L G LSHyp U L E + ˙ G LSHyp U L E + ˙ G = ˙ Y
45 44 fveq2d φ L G LSHyp U L E + ˙ G LSHyp U ˙ L E + ˙ G = ˙ ˙ Y
46 45 fveq2d φ L G LSHyp U L E + ˙ G LSHyp U ˙ ˙ L E + ˙ G = ˙ ˙ ˙ Y
47 33 46 44 3eqtr4d φ L G LSHyp U L E + ˙ G LSHyp U ˙ ˙ L E + ˙ G = L E + ˙ G
48 17 19 18 1 21 dochoc1 φ ˙ ˙ V = V
49 48 ad2antrr φ L G LSHyp U L E + ˙ G = V ˙ ˙ V = V
50 simpr φ L G LSHyp U L E + ˙ G = V L E + ˙ G = V
51 50 fveq2d φ L G LSHyp U L E + ˙ G = V ˙ L E + ˙ G = ˙ V
52 51 fveq2d φ L G LSHyp U L E + ˙ G = V ˙ ˙ L E + ˙ G = ˙ ˙ V
53 49 52 50 3eqtr4d φ L G LSHyp U L E + ˙ G = V ˙ ˙ L E + ˙ G = L E + ˙ G
54 17 19 21 dvhlmod φ U LMod
55 8 9 10 54 13 14 ldualvaddcl φ E + ˙ G F
56 1 36 8 16 37 55 lkrshpor φ L E + ˙ G LSHyp U L E + ˙ G = V
57 56 adantr φ L G LSHyp U L E + ˙ G LSHyp U L E + ˙ G = V
58 47 53 57 mpjaodan φ L G LSHyp U ˙ ˙ L E + ˙ G = L E + ˙ G
59 48 adantr φ L G = V ˙ ˙ V = V
60 1 8 16 54 55 lkrssv φ L E + ˙ G V
61 60 adantr φ L G = V L E + ˙ G V
62 simpr φ L G = V L G = V
63 34 adantr φ L G = V L G L E + ˙ G
64 62 63 eqsstrrd φ L G = V V L E + ˙ G
65 61 64 eqssd φ L G = V L E + ˙ G = V
66 65 fveq2d φ L G = V ˙ L E + ˙ G = ˙ V
67 66 fveq2d φ L G = V ˙ ˙ L E + ˙ G = ˙ ˙ V
68 59 67 65 3eqtr4d φ L G = V ˙ ˙ L E + ˙ G = L E + ˙ G
69 1 36 8 16 37 14 lkrshpor φ L G LSHyp U L G = V
70 58 68 69 mpjaodan φ ˙ ˙ L E + ˙ G = L E + ˙ G