Metamath Proof Explorer


Theorem mapdh6dN

Description: Lemmma for mapdh6N . (Contributed by NM, 1-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh.q Q=0C
mapdh.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
mapdh.h H=LHypK
mapdh.m M=mapdKW
mapdh.u U=DVecHKW
mapdh.v V=BaseU
mapdh.s -˙=-U
mapdhc.o 0˙=0U
mapdh.n N=LSpanU
mapdh.c C=LCDualKW
mapdh.d D=BaseC
mapdh.r R=-C
mapdh.j J=LSpanC
mapdh.k φKHLWH
mapdhc.f φFD
mapdh.mn φMNX=JF
mapdhcl.x φXV0˙
mapdh.p +˙=+U
mapdh.a ˙=+C
mapdh6d.xn φ¬XNYZ
mapdh6d.yz φNY=NZ
mapdh6d.y φYV0˙
mapdh6d.z φZV0˙
mapdh6d.w φwV0˙
mapdh6d.wn φ¬wNXY
Assertion mapdh6dN φIXFw+˙Y+˙Z=IXFw˙IXFY+˙Z

Proof

Step Hyp Ref Expression
1 mapdh.q Q=0C
2 mapdh.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
3 mapdh.h H=LHypK
4 mapdh.m M=mapdKW
5 mapdh.u U=DVecHKW
6 mapdh.v V=BaseU
7 mapdh.s -˙=-U
8 mapdhc.o 0˙=0U
9 mapdh.n N=LSpanU
10 mapdh.c C=LCDualKW
11 mapdh.d D=BaseC
12 mapdh.r R=-C
13 mapdh.j J=LSpanC
14 mapdh.k φKHLWH
15 mapdhc.f φFD
16 mapdh.mn φMNX=JF
17 mapdhcl.x φXV0˙
18 mapdh.p +˙=+U
19 mapdh.a ˙=+C
20 mapdh6d.xn φ¬XNYZ
21 mapdh6d.yz φNY=NZ
22 mapdh6d.y φYV0˙
23 mapdh6d.z φZV0˙
24 mapdh6d.w φwV0˙
25 mapdh6d.wn φ¬wNXY
26 3 10 14 lcdlmod φCLMod
27 24 eldifad φwV
28 3 5 14 dvhlvec φULVec
29 17 eldifad φXV
30 22 eldifad φYV
31 6 9 28 27 29 30 25 lspindpi φNwNXNwNY
32 31 simpld φNwNX
33 32 necomd φNXNw
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 27 33 mapdhcl φIXFwD
35 11 19 1 lmod0vrid CLModIXFwDIXFw˙Q=IXFw
36 26 34 35 syl2anc φIXFw˙Q=IXFw
37 36 adantr φY+˙Z=0˙IXFw˙Q=IXFw
38 oteq3 Y+˙Z=0˙XFY+˙Z=XF0˙
39 38 fveq2d Y+˙Z=0˙IXFY+˙Z=IXF0˙
40 1 2 8 17 15 mapdhval0 φIXF0˙=Q
41 39 40 sylan9eqr φY+˙Z=0˙IXFY+˙Z=Q
42 41 oveq2d φY+˙Z=0˙IXFw˙IXFY+˙Z=IXFw˙Q
43 oveq2 Y+˙Z=0˙w+˙Y+˙Z=w+˙0˙
44 3 5 14 dvhlmod φULMod
45 6 18 8 lmod0vrid ULModwVw+˙0˙=w
46 44 27 45 syl2anc φw+˙0˙=w
47 43 46 sylan9eqr φY+˙Z=0˙w+˙Y+˙Z=w
48 47 oteq3d φY+˙Z=0˙XFw+˙Y+˙Z=XFw
49 48 fveq2d φY+˙Z=0˙IXFw+˙Y+˙Z=IXFw
50 37 42 49 3eqtr4rd φY+˙Z=0˙IXFw+˙Y+˙Z=IXFw˙IXFY+˙Z
51 14 adantr φY+˙Z0˙KHLWH
52 15 adantr φY+˙Z0˙FD
53 16 adantr φY+˙Z0˙MNX=JF
54 17 adantr φY+˙Z0˙XV0˙
55 24 adantr φY+˙Z0˙wV0˙
56 23 eldifad φZV
57 6 18 lmodvacl ULModYVZVY+˙ZV
58 44 30 56 57 syl3anc φY+˙ZV
59 58 anim1i φY+˙Z0˙Y+˙ZVY+˙Z0˙
60 eldifsn Y+˙ZV0˙Y+˙ZVY+˙Z0˙
61 59 60 sylibr φY+˙Z0˙Y+˙ZV0˙
62 6 9 28 29 30 56 20 lspindpi φNXNYNXNZ
63 62 simpld φNXNY
64 6 18 8 9 28 17 22 23 24 21 63 25 mapdindp1 φNXNY+˙Z
65 6 18 8 9 28 17 22 23 24 21 63 25 mapdindp2 φ¬wNXY+˙Z
66 6 8 9 28 17 58 27 64 65 lspindp1 φNwNY+˙Z¬XNwY+˙Z
67 66 simprd φ¬XNwY+˙Z
68 67 adantr φY+˙Z0˙¬XNwY+˙Z
69 31 simprd φNwNY
70 6 8 9 28 24 30 69 lspsnne1 φ¬wNY
71 eqid LSSumU=LSSumU
72 6 9 71 44 30 56 lsmpr φNYZ=NYLSSumUNZ
73 21 oveq2d φNYLSSumUNY=NYLSSumUNZ
74 eqid LSubSpU=LSubSpU
75 6 74 9 lspsncl ULModYVNYLSubSpU
76 44 30 75 syl2anc φNYLSubSpU
77 74 lsssubg ULModNYLSubSpUNYSubGrpU
78 44 76 77 syl2anc φNYSubGrpU
79 71 lsmidm NYSubGrpUNYLSSumUNY=NY
80 78 79 syl φNYLSSumUNY=NY
81 72 73 80 3eqtr2d φNYZ=NY
82 70 81 neleqtrrd φ¬wNYZ
83 6 18 9 44 30 56 27 82 lspindp4 φ¬wNYY+˙Z
84 6 9 28 27 30 58 83 lspindpi φNwNYNwNY+˙Z
85 84 simprd φNwNY+˙Z
86 85 adantr φY+˙Z0˙NwNY+˙Z
87 eqidd φY+˙Z0˙IXFw=IXFw
88 eqidd φY+˙Z0˙IXFY+˙Z=IXFY+˙Z
89 1 2 3 4 5 6 7 8 9 10 11 12 13 51 52 53 54 18 19 55 61 68 86 87 88 mapdh6aN φY+˙Z0˙IXFw+˙Y+˙Z=IXFw˙IXFY+˙Z
90 50 89 pm2.61dane φIXFw+˙Y+˙Z=IXFw˙IXFY+˙Z