Metamath Proof Explorer


Theorem lclkrlem2v

Description: Lemma for lclkr . When the hypotheses of lclkrlem2u and lclkrlem2u are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid , which requires the orthomodular law dihoml4 (Lemma 3.3 of Holland95 p. 214). (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v V=BaseU
lclkrlem2m.t ·˙=U
lclkrlem2m.s S=ScalarU
lclkrlem2m.q ×˙=S
lclkrlem2m.z 0˙=0S
lclkrlem2m.i I=invrS
lclkrlem2m.m -˙=-U
lclkrlem2m.f F=LFnlU
lclkrlem2m.d D=LDualU
lclkrlem2m.p +˙=+D
lclkrlem2m.x φXV
lclkrlem2m.y φYV
lclkrlem2m.e φEF
lclkrlem2m.g φGF
lclkrlem2n.n N=LSpanU
lclkrlem2n.l L=LKerU
lclkrlem2o.h H=LHypK
lclkrlem2o.o ˙=ocHKW
lclkrlem2o.u U=DVecHKW
lclkrlem2o.a ˙=LSSumU
lclkrlem2o.k φKHLWH
lclkrlem2q.le φLE=˙X
lclkrlem2q.lg φLG=˙Y
lclkrlem2v.j φE+˙GX=0˙
lclkrlem2v.k φE+˙GY=0˙
Assertion lclkrlem2v φLE+˙G=V

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v V=BaseU
2 lclkrlem2m.t ·˙=U
3 lclkrlem2m.s S=ScalarU
4 lclkrlem2m.q ×˙=S
5 lclkrlem2m.z 0˙=0S
6 lclkrlem2m.i I=invrS
7 lclkrlem2m.m -˙=-U
8 lclkrlem2m.f F=LFnlU
9 lclkrlem2m.d D=LDualU
10 lclkrlem2m.p +˙=+D
11 lclkrlem2m.x φXV
12 lclkrlem2m.y φYV
13 lclkrlem2m.e φEF
14 lclkrlem2m.g φGF
15 lclkrlem2n.n N=LSpanU
16 lclkrlem2n.l L=LKerU
17 lclkrlem2o.h H=LHypK
18 lclkrlem2o.o ˙=ocHKW
19 lclkrlem2o.u U=DVecHKW
20 lclkrlem2o.a ˙=LSSumU
21 lclkrlem2o.k φKHLWH
22 lclkrlem2q.le φLE=˙X
23 lclkrlem2q.lg φLG=˙Y
24 lclkrlem2v.j φE+˙GX=0˙
25 lclkrlem2v.k φE+˙GY=0˙
26 17 19 21 dvhlmod φULMod
27 8 9 10 26 13 14 ldualvaddcl φE+˙GF
28 1 8 16 26 27 lkrssv φLE+˙GV
29 eqid LSubSpU=LSubSpU
30 1 29 15 26 11 12 lspprcl φNXYLSubSpU
31 eqid DIsoHKW=DIsoHKW
32 17 19 1 15 31 21 11 12 dihprrn φNXYranDIsoHKW
33 1 29 lssss NXYLSubSpUNXYV
34 30 33 syl φNXYV
35 17 31 19 1 18 21 34 dochoccl φNXYranDIsoHKW˙˙NXY=NXY
36 32 35 mpbid φ˙˙NXY=NXY
37 17 18 19 1 29 20 21 30 36 dochexmid φNXY˙˙NXY=V
38 17 19 21 dvhlvec φULVec
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38 24 25 lclkrlem2n φNXYLE+˙G
40 11 snssd φXV
41 12 snssd φYV
42 17 19 1 18 dochdmj1 KHLWHXVYV˙XY=˙X˙Y
43 21 40 41 42 syl3anc φ˙XY=˙X˙Y
44 df-pr XY=XY
45 44 fveq2i NXY=NXY
46 45 fveq2i ˙NXY=˙NXY
47 40 41 unssd φXYV
48 17 19 18 1 15 21 47 dochocsp φ˙NXY=˙XY
49 46 48 eqtrid φ˙NXY=˙XY
50 22 23 ineq12d φLELG=˙X˙Y
51 43 49 50 3eqtr4d φ˙NXY=LELG
52 8 16 9 10 26 13 14 lkrin φLELGLE+˙G
53 51 52 eqsstrd φ˙NXYLE+˙G
54 29 lsssssubg ULModLSubSpUSubGrpU
55 26 54 syl φLSubSpUSubGrpU
56 55 30 sseldd φNXYSubGrpU
57 17 19 1 29 18 dochlss KHLWHNXYV˙NXYLSubSpU
58 21 34 57 syl2anc φ˙NXYLSubSpU
59 55 58 sseldd φ˙NXYSubGrpU
60 8 16 29 lkrlss ULModE+˙GFLE+˙GLSubSpU
61 26 27 60 syl2anc φLE+˙GLSubSpU
62 55 61 sseldd φLE+˙GSubGrpU
63 20 lsmlub NXYSubGrpU˙NXYSubGrpULE+˙GSubGrpUNXYLE+˙G˙NXYLE+˙GNXY˙˙NXYLE+˙G
64 56 59 62 63 syl3anc φNXYLE+˙G˙NXYLE+˙GNXY˙˙NXYLE+˙G
65 39 53 64 mpbi2and φNXY˙˙NXYLE+˙G
66 37 65 eqsstrrd φVLE+˙G
67 28 66 eqssd φLE+˙G=V