Metamath Proof Explorer


Theorem hdmap11lem2

Description: Lemma for hdmapadd . (Contributed by NM, 26-May-2015)

Ref Expression
Hypotheses hdmap11.h H=LHypK
hdmap11.u U=DVecHKW
hdmap11.v V=BaseU
hdmap11.p +˙=+U
hdmap11.c C=LCDualKW
hdmap11.a ˙=+C
hdmap11.s S=HDMapKW
hdmap11.k φKHLWH
hdmap11.x φXV
hdmap11.y φYV
hdmap11.e E=IBaseKILTrnKW
hdmap11.o 0˙=0U
hdmap11.n N=LSpanU
hdmap11.d D=BaseC
hdmap11.l L=LSpanC
hdmap11.m M=mapdKW
hdmap11.j J=HVMapKW
hdmap11.i I=HDMap1KW
Assertion hdmap11lem2 φSX+˙Y=SX˙SY

Proof

Step Hyp Ref Expression
1 hdmap11.h H=LHypK
2 hdmap11.u U=DVecHKW
3 hdmap11.v V=BaseU
4 hdmap11.p +˙=+U
5 hdmap11.c C=LCDualKW
6 hdmap11.a ˙=+C
7 hdmap11.s S=HDMapKW
8 hdmap11.k φKHLWH
9 hdmap11.x φXV
10 hdmap11.y φYV
11 hdmap11.e E=IBaseKILTrnKW
12 hdmap11.o 0˙=0U
13 hdmap11.n N=LSpanU
14 hdmap11.d D=BaseC
15 hdmap11.l L=LSpanC
16 hdmap11.m M=mapdKW
17 hdmap11.j J=HVMapKW
18 hdmap11.i I=HDMap1KW
19 1 2 3 13 8 9 10 dvh3dim φzV¬zNXY
20 19 adantr φENXYzV¬zNXY
21 eqid LSubSpU=LSubSpU
22 1 2 8 dvhlmod φULMod
23 22 adantr φENXYULMod
24 3 21 13 22 9 10 lspprcl φNXYLSubSpU
25 24 adantr φENXYNXYLSubSpU
26 simpr φENXYENXY
27 21 13 23 25 26 lspsnel5a φENXYNENXY
28 27 ssneld φENXY¬zNXY¬zNE
29 28 ancld φENXY¬zNXY¬zNXY¬zNE
30 29 reximdv φENXYzV¬zNXYzV¬zNXY¬zNE
31 20 30 mpd φENXYzV¬zNXY¬zNE
32 eqid BaseK=BaseK
33 eqid LTrnKW=LTrnKW
34 1 32 33 2 3 12 11 8 dvheveccl φEV0˙
35 34 eldifad φEV
36 1 2 3 13 8 35 10 dvh3dim φzV¬zNEY
37 36 adantr φX=0˙zV¬zNEY
38 preq1 X=0˙XY=0˙Y
39 prcom 0˙Y=Y0˙
40 38 39 eqtrdi X=0˙XY=Y0˙
41 40 fveq2d X=0˙NXY=NY0˙
42 3 12 13 22 10 lsppr0 φNY0˙=NY
43 41 42 sylan9eqr φX=0˙NXY=NY
44 3 21 13 22 35 10 lspprcl φNEYLSubSpU
45 3 13 22 35 10 lspprid2 φYNEY
46 21 13 22 44 45 lspsnel5a φNYNEY
47 46 adantr φX=0˙NYNEY
48 43 47 eqsstrd φX=0˙NXYNEY
49 48 ssneld φX=0˙¬zNEY¬zNXY
50 3 13 22 35 10 lspprid1 φENEY
51 21 13 22 44 50 lspsnel5a φNENEY
52 51 adantr φX=0˙NENEY
53 52 ssneld φX=0˙¬zNEY¬zNE
54 49 53 jcad φX=0˙¬zNEY¬zNXY¬zNE
55 54 reximdv φX=0˙zV¬zNEYzV¬zNXY¬zNE
56 37 55 mpd φX=0˙zV¬zNXY¬zNE
57 56 adantlr φ¬ENXYX=0˙zV¬zNXY¬zNE
58 3 4 lmodvacl ULModEVXVE+˙XV
59 22 35 9 58 syl3anc φE+˙XV
60 59 ad2antrr φ¬ENXYX0˙E+˙XV
61 22 ad2antrr φ¬ENXYX0˙ULMod
62 24 ad2antrr φ¬ENXYX0˙NXYLSubSpU
63 3 13 22 9 10 lspprid1 φXNXY
64 63 ad2antrr φ¬ENXYX0˙XNXY
65 35 ad2antrr φ¬ENXYX0˙EV
66 simplr φ¬ENXYX0˙¬ENXY
67 3 4 21 61 62 64 65 66 lssvancl2 φ¬ENXYX0˙¬E+˙XNXY
68 3 21 13 lspsncl ULModEVNELSubSpU
69 22 35 68 syl2anc φNELSubSpU
70 69 ad2antrr φ¬ENXYX0˙NELSubSpU
71 3 13 lspsnid ULModEVENE
72 22 35 71 syl2anc φENE
73 72 ad2antrr φ¬ENXYX0˙ENE
74 9 ad2antrr φ¬ENXYX0˙XV
75 1 2 8 dvhlvec φULVec
76 75 ad2antrr φ¬ENXYX0˙ULVec
77 simpr φ¬ENXYX0˙X0˙
78 eldifsn XV0˙XVX0˙
79 74 77 78 sylanbrc φ¬ENXYX0˙XV0˙
80 21 13 22 24 63 lspsnel5a φNXNXY
81 80 sseld φENXENXY
82 81 con3dimp φ¬ENXY¬ENX
83 82 adantr φ¬ENXYX0˙¬ENX
84 3 12 13 76 65 79 83 lspsnnecom φ¬ENXYX0˙¬XNE
85 3 4 21 61 70 73 74 84 lssvancl1 φ¬ENXYX0˙¬E+˙XNE
86 eleq1 z=E+˙XzNXYE+˙XNXY
87 86 notbid z=E+˙X¬zNXY¬E+˙XNXY
88 eleq1 z=E+˙XzNEE+˙XNE
89 88 notbid z=E+˙X¬zNE¬E+˙XNE
90 87 89 anbi12d z=E+˙X¬zNXY¬zNE¬E+˙XNXY¬E+˙XNE
91 90 rspcev E+˙XV¬E+˙XNXY¬E+˙XNEzV¬zNXY¬zNE
92 60 67 85 91 syl12anc φ¬ENXYX0˙zV¬zNXY¬zNE
93 57 92 pm2.61dane φ¬ENXYzV¬zNXY¬zNE
94 31 93 pm2.61dan φzV¬zNXY¬zNE
95 8 3ad2ant1 φzV¬zNXY¬zNEKHLWH
96 9 3ad2ant1 φzV¬zNXY¬zNEXV
97 10 3ad2ant1 φzV¬zNXY¬zNEYV
98 simp2 φzV¬zNXY¬zNEzV
99 simp3l φzV¬zNXY¬zNE¬zNXY
100 22 3ad2ant1 φzV¬zNXY¬zNEULMod
101 35 3ad2ant1 φzV¬zNXY¬zNEEV
102 simp3r φzV¬zNXY¬zNE¬zNE
103 3 13 100 98 101 102 lspsnne2 φzV¬zNXY¬zNENzNE
104 1 2 3 4 5 6 7 95 96 97 11 12 13 14 15 16 17 18 98 99 103 hdmap11lem1 φzV¬zNXY¬zNESX+˙Y=SX˙SY
105 104 rexlimdv3a φzV¬zNXY¬zNESX+˙Y=SX˙SY
106 94 105 mpd φSX+˙Y=SX˙SY