# Metamath Proof Explorer

## Theorem dihopelvalcpre

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dihopelvalcp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihopelvalcp.l
dihopelvalcp.j
dihopelvalcp.m
dihopelvalcp.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihopelvalcp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihopelvalcp.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dihopelvalcp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dihopelvalcp.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dihopelvalcp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dihopelvalcp.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihopelvalcp.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
dihopelvalcp.f ${⊢}{F}\in \mathrm{V}$
dihopelvalcp.s ${⊢}{S}\in \mathrm{V}$
dihopelvalcp.z ${⊢}{Z}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dihopelvalcp.n ${⊢}{N}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
dihopelvalcp.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dihopelvalcp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihopelvalcp.d
dihopelvalcp.v ${⊢}{V}=\mathrm{LSubSp}\left({U}\right)$
dihopelvalcp.y
dihopelvalcp.o ${⊢}{O}=\left({a}\in {E},{b}\in {E}⟼\left({h}\in {T}⟼{a}\left({h}\right)\circ {b}\left({h}\right)\right)\right)$
Assertion dihopelvalcpre

### Proof

Step Hyp Ref Expression
1 dihopelvalcp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihopelvalcp.l
3 dihopelvalcp.j
4 dihopelvalcp.m
5 dihopelvalcp.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 dihopelvalcp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 dihopelvalcp.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
8 dihopelvalcp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
9 dihopelvalcp.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
10 dihopelvalcp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
11 dihopelvalcp.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
12 dihopelvalcp.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
13 dihopelvalcp.f ${⊢}{F}\in \mathrm{V}$
14 dihopelvalcp.s ${⊢}{S}\in \mathrm{V}$
15 dihopelvalcp.z ${⊢}{Z}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
16 dihopelvalcp.n ${⊢}{N}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
17 dihopelvalcp.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
18 dihopelvalcp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
19 dihopelvalcp.d
20 dihopelvalcp.v ${⊢}{V}=\mathrm{LSubSp}\left({U}\right)$
21 dihopelvalcp.y
22 dihopelvalcp.o ${⊢}{O}=\left({a}\in {E},{b}\in {E}⟼\left({h}\in {T}⟼{a}\left({h}\right)\circ {b}\left({h}\right)\right)\right)$
23 1 2 3 4 5 6 11 16 17 18 21 dihvalcq
24 23 eleq2d
25 simp1
26 simp3l
27 2 5 6 18 17 20 diclss
28 25 26 27 syl2anc
29 simp1l
30 29 hllatd
31 simp2l
32 simp1r
33 1 6 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
34 32 33 syl
35 1 4 latmcl
36 30 31 34 35 syl3anc
37 1 2 4 latmle2
38 30 31 34 37 syl3anc
39 1 2 6 18 16 20 diblss
40 25 36 38 39 syl12anc
41 6 18 19 20 21 dvhopellsm
42 25 28 40 41 syl3anc
43 vex ${⊢}{x}\in \mathrm{V}$
44 vex ${⊢}{y}\in \mathrm{V}$
45 2 5 6 7 8 10 17 12 43 44 dicopelval2
46 25 26 45 syl2anc
47 1 2 6 8 9 15 16 dibopelval3
48 25 36 38 47 syl12anc
49 46 48 anbi12d
50 49 anbi1d
51 simpl1
52 simprll
53 simprlr
54 2 5 6 7 lhpocnel2
55 51 54 syl
56 simpl3l
57 2 5 6 8 12 ltrniotacl
58 51 55 56 57 syl3anc
59 6 8 10 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {y}\in {E}\wedge {G}\in {T}\right)\to {y}\left({G}\right)\in {T}$
60 51 53 58 59 syl3anc
61 52 60 eqeltrd
62 simprll
64 simprrr
65 1 6 8 10 15 tendo0cl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {Z}\in {E}$
66 51 65 syl
67 64 66 eqeltrd
68 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
69 eqid ${⊢}{+}_{\mathrm{Scalar}\left({U}\right)}={+}_{\mathrm{Scalar}\left({U}\right)}$
70 6 8 10 18 68 19 69 dvhopvadd
71 51 61 53 63 67 70 syl122anc
72 6 8 10 18 68 22 69 dvhfplusr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {+}_{\mathrm{Scalar}\left({U}\right)}={O}$
73 51 72 syl
74 73 oveqd
75 74 opeq2d
76 71 75 eqtrd
77 76 eqeq2d
78 13 14 opth ${⊢}⟨{F},{S}⟩=⟨{x}\circ {z},{y}{O}{w}⟩↔\left({F}={x}\circ {z}\wedge {S}={y}{O}{w}\right)$
79 64 oveq2d
80 1 6 8 10 15 22 tendo0plr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {y}\in {E}\right)\to {y}{O}{Z}={y}$
81 51 53 80 syl2anc
82 79 81 eqtrd
83 82 eqeq2d
84 83 anbi2d
85 78 84 syl5bb
86 77 85 bitrd
87 86 pm5.32da
88 simplll
90 simprrr
91 90 fveq1d
92 89 91 eqtr4d
93 90 eqcomd
94 coass ${⊢}\left({{S}\left({G}\right)}^{-1}\circ {S}\left({G}\right)\right)\circ {z}={{S}\left({G}\right)}^{-1}\circ \left({S}\left({G}\right)\circ {z}\right)$
95 simpl1
96 simpllr
98 90 97 eqeltrd
100 6 8 10 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {G}\in {T}\right)\to {S}\left({G}\right)\in {T}$
101 95 98 99 100 syl3anc
102 1 6 8 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\left({G}\right)\in {T}\right)\to {S}\left({G}\right):{B}\underset{1-1 onto}{⟶}{B}$
103 95 101 102 syl2anc
104 f1ococnv1 ${⊢}{S}\left({G}\right):{B}\underset{1-1 onto}{⟶}{B}\to {{S}\left({G}\right)}^{-1}\circ {S}\left({G}\right)={\mathrm{I}↾}_{{B}}$
105 103 104 syl
106 105 coeq1d
108 1 6 8 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {z}\in {T}\right)\to {z}:{B}\underset{1-1 onto}{⟶}{B}$
109 95 107 108 syl2anc
110 f1of ${⊢}{z}:{B}\underset{1-1 onto}{⟶}{B}\to {z}:{B}⟶{B}$
111 fcoi2 ${⊢}{z}:{B}⟶{B}\to \left({\mathrm{I}↾}_{{B}}\right)\circ {z}={z}$
112 109 110 111 3syl
113 106 112 eqtr2d
114 simprrl
115 92 coeq1d
116 114 115 eqtrd
117 116 coeq1d
118 6 8 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\left({G}\right)\in {T}\right)\to {{S}\left({G}\right)}^{-1}\in {T}$
119 95 101 118 syl2anc
120 6 8 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\left({G}\right)\in {T}\wedge {z}\in {T}\right)\to {S}\left({G}\right)\circ {z}\in {T}$
121 95 101 107 120 syl3anc
122 6 8 ltrncom ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {{S}\left({G}\right)}^{-1}\in {T}\wedge {S}\left({G}\right)\circ {z}\in {T}\right)\to {{S}\left({G}\right)}^{-1}\circ \left({S}\left({G}\right)\circ {z}\right)=\left({S}\left({G}\right)\circ {z}\right)\circ {{S}\left({G}\right)}^{-1}$
123 95 119 121 122 syl3anc
124 117 123 eqtr4d
125 94 113 124 3eqtr4a
126 simplrr
128 125 127 jca
129 92 93 128 jca31
130 129 ex
131 130 pm4.71rd
132 87 131 bitrd
133 simprrl
134 simpll1
137 134 54 syl
138 simpl3l
140 134 137 139 57 syl3anc
141 134 136 140 59 syl3anc
142 135 141 eqeltrd
144 6 8 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in {T}\wedge {z}\in {T}\right)\to {x}\circ {z}\in {T}$
145 134 142 143 144 syl3anc
146 133 145 eqeltrd
147 simpl1l
149 148 hllatd
150 1 6 8 9 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {z}\in {T}\right)\to {R}\left({z}\right)\in {B}$
151 134 143 150 syl2anc
152 simpl2l
154 simpl1r
156 155 33 syl
157 149 153 156 35 syl3anc
158 simprlr
160 1 2 4 latmle1
161 149 153 156 160 syl3anc
162 1 2 149 151 157 153 159 161 lattrd
163 146 136 162 jca31
164 simprll
166 simprlr
168 167 fveq1d
169 165 168 eqtr4d
170 simprlr
171 169 170 jca
172 simprrl
174 simpll1
175 simprll
176 167 170 eqeltrrd
177 174 54 syl
179 174 177 178 57 syl3anc
180 174 176 179 100 syl3anc
181 174 180 118 syl2anc
182 6 8 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {{S}\left({G}\right)}^{-1}\in {T}\right)\to {F}\circ {{S}\left({G}\right)}^{-1}\in {T}$
183 174 175 181 182 syl3anc
184 173 183 eqeltrd
185 simprr
186 2 6 8 9 trlle
187 174 184 186 syl2anc
189 188 hllatd
190 174 184 150 syl2anc
193 192 33 syl
194 1 2 4 latlem12
195 189 190 191 193 194 syl13anc
196 185 187 195 mpbi2and
197 simprrr
199 184 196 198 jca31
200 174 180 102 syl2anc
201 200 104 syl
202 201 coeq2d
203 1 6 8 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
204 174 175 203 syl2anc
205 f1of ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{B}\to {F}:{B}⟶{B}$
206 fcoi1 ${⊢}{F}:{B}⟶{B}\to {F}\circ \left({\mathrm{I}↾}_{{B}}\right)={F}$
207 204 205 206 3syl
208 202 207 eqtr2d
209 coass ${⊢}\left({F}\circ {{S}\left({G}\right)}^{-1}\right)\circ {S}\left({G}\right)={F}\circ \left({{S}\left({G}\right)}^{-1}\circ {S}\left({G}\right)\right)$
210 208 209 syl6eqr
211 6 8 ltrncom ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\left({G}\right)\in {T}\wedge {F}\circ {{S}\left({G}\right)}^{-1}\in {T}\right)\to {S}\left({G}\right)\circ \left({F}\circ {{S}\left({G}\right)}^{-1}\right)=\left({F}\circ {{S}\left({G}\right)}^{-1}\right)\circ {S}\left({G}\right)$
212 174 180 183 211 syl3anc
213 210 212 eqtr4d
214 165 173 coeq12d
215 213 214 eqtr4d
216 167 eqcomd
217 215 216 jca
218 171 199 217 jca31
219 163 218 impbida
220 219 pm5.32da
221 df-3an
222 220 221 syl6bbr
223 50 132 222 3bitrd
224 223 4exbidv
225 fvex ${⊢}{S}\left({G}\right)\in \mathrm{V}$
226 225 cnvex ${⊢}{{S}\left({G}\right)}^{-1}\in \mathrm{V}$
227 13 226 coex ${⊢}{F}\circ {{S}\left({G}\right)}^{-1}\in \mathrm{V}$
228 8 fvexi ${⊢}{T}\in \mathrm{V}$
229 228 mptex ${⊢}\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\in \mathrm{V}$
230 15 229 eqeltri ${⊢}{Z}\in \mathrm{V}$
231 biidd
232 eleq1 ${⊢}{y}={S}\to \left({y}\in {E}↔{S}\in {E}\right)$
233 232 anbi2d ${⊢}{y}={S}\to \left(\left({F}\in {T}\wedge {y}\in {E}\right)↔\left({F}\in {T}\wedge {S}\in {E}\right)\right)$
234 233 anbi1d
235 fveq2 ${⊢}{z}={F}\circ {{S}\left({G}\right)}^{-1}\to {R}\left({z}\right)={R}\left({F}\circ {{S}\left({G}\right)}^{-1}\right)$
236 235 breq1d
237 236 anbi2d
238 biidd
239 225 14 227 230 231 234 237 238 ceqsex4v
240 224 239 syl6bb
241 24 42 240 3bitrd