Metamath Proof Explorer


Theorem dih1dimatlem

Description: Lemma for dih1dimat . (Contributed by NM, 10-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h H=LHypK
dih1dimat.u U=DVecHKW
dih1dimat.i I=DIsoHKW
dih1dimat.a A=LSAtomsU
dih1dimat.b B=BaseK
dih1dimat.l ˙=K
dih1dimat.c C=AtomsK
dih1dimat.p P=ocKW
dih1dimat.t T=LTrnKW
dih1dimat.r R=trLKW
dih1dimat.e E=TEndoKW
dih1dimat.o O=hTIB
dih1dimat.d F=ScalarU
dih1dimat.j J=invrF
dih1dimat.v V=BaseU
dih1dimat.m ·˙=U
dih1dimat.s S=LSubSpU
dih1dimat.n N=LSpanU
dih1dimat.z 0˙=0U
dih1dimat.g G=ιhT|hP=JsfP
Assertion dih1dimatlem KHLWHDADranI

Proof

Step Hyp Ref Expression
1 dih1dimat.h H=LHypK
2 dih1dimat.u U=DVecHKW
3 dih1dimat.i I=DIsoHKW
4 dih1dimat.a A=LSAtomsU
5 dih1dimat.b B=BaseK
6 dih1dimat.l ˙=K
7 dih1dimat.c C=AtomsK
8 dih1dimat.p P=ocKW
9 dih1dimat.t T=LTrnKW
10 dih1dimat.r R=trLKW
11 dih1dimat.e E=TEndoKW
12 dih1dimat.o O=hTIB
13 dih1dimat.d F=ScalarU
14 dih1dimat.j J=invrF
15 dih1dimat.v V=BaseU
16 dih1dimat.m ·˙=U
17 dih1dimat.s S=LSubSpU
18 dih1dimat.n N=LSpanU
19 dih1dimat.z 0˙=0U
20 dih1dimat.g G=ιhT|hP=JsfP
21 id KHLWHKHLWH
22 1 2 21 dvhlvec KHLWHULVec
23 15 18 19 4 islsat ULVecDAvV0˙D=Nv
24 22 23 syl KHLWHDAvV0˙D=Nv
25 24 biimpa KHLWHDAvV0˙D=Nv
26 eldifi vV0˙vV
27 1 9 11 2 15 dvhvbase KHLWHV=T×E
28 27 eleq2d KHLWHvVvT×E
29 26 28 syl5ib KHLWHvV0˙vT×E
30 29 imp KHLWHvV0˙vT×E
31 simpr KHLWHfTsEs=Os=O
32 31 opeq2d KHLWHfTsEs=Ofs=fO
33 32 sneqd KHLWHfTsEs=Ofs=fO
34 33 fveq2d KHLWHfTsEs=ONfs=NfO
35 simpl KHLWHfTKHLWH
36 5 1 9 10 trlcl KHLWHfTRfB
37 6 1 9 10 trlle KHLWHfTRf˙W
38 eqid DIsoBKW=DIsoBKW
39 5 6 1 3 38 dihvalb KHLWHRfBRf˙WIRf=DIsoBKWRf
40 35 36 37 39 syl12anc KHLWHfTIRf=DIsoBKWRf
41 5 1 9 10 12 2 38 18 dib1dim2 KHLWHfTDIsoBKWRf=NfO
42 40 41 eqtr2d KHLWHfTNfO=IRf
43 5 1 3 2 17 dihf11 KHLWHI:B1-1S
44 43 adantr KHLWHfTI:B1-1S
45 f1fn I:B1-1SIFnB
46 44 45 syl KHLWHfTIFnB
47 fnfvelrn IFnBRfBIRfranI
48 46 36 47 syl2anc KHLWHfTIRfranI
49 42 48 eqeltrd KHLWHfTNfOranI
50 49 adantrr KHLWHfTsENfOranI
51 50 adantr KHLWHfTsEs=ONfOranI
52 34 51 eqeltrd KHLWHfTsEs=ONfsranI
53 simpll KHLWHfTsEsOKHLWH
54 eqid BaseF=BaseF
55 1 11 2 13 54 dvhbase KHLWHBaseF=E
56 53 55 syl KHLWHfTsEsOBaseF=E
57 56 rexeqdv KHLWHfTsEsOtBaseFu=t·˙fstEu=t·˙fs
58 simplll KHLWHfTsEsOtEKHLWH
59 simpr KHLWHfTsEsOtEtE
60 opelxpi fTsEfsT×E
61 60 ad3antlr KHLWHfTsEsOtEfsT×E
62 1 9 11 2 16 dvhvscacl KHLWHtEfsT×Et·˙fsT×E
63 58 59 61 62 syl12anc KHLWHfTsEsOtEt·˙fsT×E
64 eleq1a t·˙fsT×Eu=t·˙fsuT×E
65 63 64 syl KHLWHfTsEsOtEu=t·˙fsuT×E
66 65 rexlimdva KHLWHfTsEsOtEu=t·˙fsuT×E
67 66 pm4.71rd KHLWHfTsEsOtEu=t·˙fsuT×EtEu=t·˙fs
68 simplrl KHLWHfTsEsOfT
69 68 adantr KHLWHfTsEsOtEfT
70 simplrr KHLWHfTsEsOsE
71 70 adantr KHLWHfTsEsOtEsE
72 1 9 11 2 16 dvhopvsca KHLWHtEfTsEt·˙fs=tfts
73 58 59 69 71 72 syl13anc KHLWHfTsEsOtEt·˙fs=tfts
74 73 eqeq2d KHLWHfTsEsOtEu=t·˙fsu=tfts
75 74 rexbidva KHLWHfTsEsOtEu=t·˙fstEu=tfts
76 75 anbi2d KHLWHfTsEsOuT×EtEu=t·˙fsuT×EtEu=tfts
77 57 67 76 3bitrd KHLWHfTsEsOtBaseFu=t·˙fsuT×EtEu=tfts
78 77 abbidv KHLWHfTsEsOu|tBaseFu=t·˙fs=u|uT×EtEu=tfts
79 df-rab uT×E|tEu=tfts=u|uT×EtEu=tfts
80 78 79 eqtr4di KHLWHfTsEsOu|tBaseFu=t·˙fs=uT×E|tEu=tfts
81 ssrab2 uT×E|tEu=tftsT×E
82 relxp RelT×E
83 relss uT×E|tEu=tftsT×ERelT×EReluT×E|tEu=tfts
84 81 82 83 mp2 ReluT×E|tEu=tfts
85 relopabv Relgr|g=rGrE
86 vex iV
87 vex pV
88 eqeq1 g=ig=rGi=rG
89 88 anbi1d g=ig=rGrEi=rGrE
90 fveq1 r=prG=pG
91 90 eqeq2d r=pi=rGi=pG
92 eleq1w r=prEpE
93 91 92 anbi12d r=pi=rGrEi=pGpE
94 86 87 89 93 opelopab ipgr|g=rGrEi=pGpE
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem0 KHLWHfTsEsOi=pGpEiTpEtEi=tfp=ts
96 95 3expa KHLWHfTsEsOi=pGpEiTpEtEi=tfp=ts
97 opelxp ipT×EiTpE
98 86 87 opth ip=tftsi=tfp=ts
99 98 rexbii tEip=tftstEi=tfp=ts
100 97 99 anbi12i ipT×EtEip=tftsiTpEtEi=tfp=ts
101 96 100 bitr4di KHLWHfTsEsOi=pGpEipT×EtEip=tfts
102 eqeq1 u=ipu=tftsip=tfts
103 102 rexbidv u=iptEu=tftstEip=tfts
104 103 elrab ipuT×E|tEu=tftsipT×EtEip=tfts
105 101 104 bitr4di KHLWHfTsEsOi=pGpEipuT×E|tEu=tfts
106 94 105 bitr2id KHLWHfTsEsOipuT×E|tEu=tftsipgr|g=rGrE
107 84 85 106 eqrelrdv KHLWHfTsEsOuT×E|tEu=tfts=gr|g=rGrE
108 80 107 eqtrd KHLWHfTsEsOu|tBaseFu=t·˙fs=gr|g=rGrE
109 1 2 53 dvhlmod KHLWHfTsEsOULMod
110 1 9 11 2 15 dvhelvbasei KHLWHfTsEfsV
111 110 adantr KHLWHfTsEsOfsV
112 13 54 15 16 18 lspsn ULModfsVNfs=u|tBaseFu=t·˙fs
113 109 111 112 syl2anc KHLWHfTsEsONfs=u|tBaseFu=t·˙fs
114 simpr KHLWHfTsEsOsO
115 5 1 9 11 12 2 13 14 tendoinvcl KHLWHsEsOJsEJsO
116 115 simpld KHLWHsEsOJsE
117 53 70 114 116 syl3anc KHLWHfTsEsOJsE
118 1 9 11 tendocl KHLWHJsEfTJsfT
119 53 117 68 118 syl3anc KHLWHfTsEsOJsfT
120 6 7 1 8 lhpocnel2 KHLWHPC¬P˙W
121 53 120 syl KHLWHfTsEsOPC¬P˙W
122 6 7 1 9 ltrnel KHLWHJsfTPC¬P˙WJsfPC¬JsfP˙W
123 53 119 121 122 syl3anc KHLWHfTsEsOJsfPC¬JsfP˙W
124 eqid DIsoCKW=DIsoCKW
125 6 7 1 124 3 dihvalcqat KHLWHJsfPC¬JsfP˙WIJsfP=DIsoCKWJsfP
126 53 123 125 syl2anc KHLWHfTsEsOIJsfP=DIsoCKWJsfP
127 6 7 1 8 9 11 124 20 dicval2 KHLWHJsfPC¬JsfP˙WDIsoCKWJsfP=gr|g=rGrE
128 53 123 127 syl2anc KHLWHfTsEsODIsoCKWJsfP=gr|g=rGrE
129 126 128 eqtrd KHLWHfTsEsOIJsfP=gr|g=rGrE
130 108 113 129 3eqtr4d KHLWHfTsEsONfs=IJsfP
131 5 1 3 dihfn KHLWHIFnB
132 131 adantr KHLWHfTsEIFnB
133 132 adantr KHLWHfTsEsOIFnB
134 simplll KHLWHfTsEsOKHL
135 hlop KHLKOP
136 134 135 syl KHLWHfTsEsOKOP
137 5 1 lhpbase WHWB
138 137 ad3antlr KHLWHfTsEsOWB
139 eqid ocK=ocK
140 5 139 opoccl KOPWBocKWB
141 136 138 140 syl2anc KHLWHfTsEsOocKWB
142 8 141 eqeltrid KHLWHfTsEsOPB
143 5 1 9 ltrncl KHLWHJsfTPBJsfPB
144 53 119 142 143 syl3anc KHLWHfTsEsOJsfPB
145 fnfvelrn IFnBJsfPBIJsfPranI
146 133 144 145 syl2anc KHLWHfTsEsOIJsfPranI
147 130 146 eqeltrd KHLWHfTsEsONfsranI
148 52 147 pm2.61dane KHLWHfTsENfsranI
149 148 ralrimivva KHLWHfTsENfsranI
150 sneq v=fsv=fs
151 150 fveq2d v=fsNv=Nfs
152 151 eleq1d v=fsNvranINfsranI
153 152 ralxp vT×ENvranIfTsENfsranI
154 149 153 sylibr KHLWHvT×ENvranI
155 154 r19.21bi KHLWHvT×ENvranI
156 30 155 syldan KHLWHvV0˙NvranI
157 eleq1a NvranID=NvDranI
158 156 157 syl KHLWHvV0˙D=NvDranI
159 158 rexlimdva KHLWHvV0˙D=NvDranI
160 159 adantr KHLWHDAvV0˙D=NvDranI
161 25 160 mpd KHLWHDADranI