Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihopelvalcpre Structured version   Unicode version

Theorem dihopelvalcpre 31947
 Description: Member of value of isomorphism H for a lattice when , given auxiliary atom . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.)
Hypotheses
Ref Expression
dihopelvalcp.b
dihopelvalcp.l
dihopelvalcp.j
dihopelvalcp.m
dihopelvalcp.a
dihopelvalcp.h
dihopelvalcp.p
dihopelvalcp.t
dihopelvalcp.r
dihopelvalcp.e
dihopelvalcp.i
dihopelvalcp.g
dihopelvalcp.f
dihopelvalcp.s
dihopelvalcp.z
dihopelvalcp.n
dihopelvalcp.c
dihopelvalcp.u
dihopelvalcp.d
dihopelvalcp.v
dihopelvalcp.y
dihopelvalcp.o
Assertion
Ref Expression
dihopelvalcpre
Distinct variable groups:   ,   ,   ,   ,,   ,,   ,,,,   ,   ,,,,   ,,,,   ,
Allowed substitution hints:   (,,)   (,,)   (,,,)   (,,)   (,,,)   (,,,)   (,,)   (,,,)   (,,,)   (,,,)   (,)   (,,,)   (,,,)   (,)   (,,,)   (,,,)   (,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)

Proof of Theorem dihopelvalcpre
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihopelvalcp.b . . . 4
2 dihopelvalcp.l . . . 4
3 dihopelvalcp.j . . . 4
4 dihopelvalcp.m . . . 4
5 dihopelvalcp.a . . . 4
6 dihopelvalcp.h . . . 4
7 dihopelvalcp.i . . . 4
8 dihopelvalcp.n . . . 4
9 dihopelvalcp.c . . . 4
10 dihopelvalcp.u . . . 4
11 dihopelvalcp.y . . . 4
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11dihvalcq 31935 . . 3
1312eleq2d 2502 . 2
14 simp1 957 . . 3
15 simp3l 985 . . . 4
16 dihopelvalcp.v . . . . 5
172, 5, 6, 10, 9, 16diclss 31892 . . . 4
1814, 15, 17syl2anc 643 . . 3
19 simp1l 981 . . . . . 6
20 hllat 30062 . . . . . 6
2119, 20syl 16 . . . . 5
22 simp2l 983 . . . . 5
23 simp1r 982 . . . . . 6
241, 6lhpbase 30696 . . . . . 6
2523, 24syl 16 . . . . 5
261, 4latmcl 14470 . . . . 5
2721, 22, 25, 26syl3anc 1184 . . . 4
281, 2, 4latmle2 14496 . . . . 5
2921, 22, 25, 28syl3anc 1184 . . . 4
301, 2, 6, 10, 8, 16diblss 31869 . . . 4
3114, 27, 29, 30syl12anc 1182 . . 3
32 dihopelvalcp.d . . . 4
336, 10, 32, 16, 11dvhopellsm 31816 . . 3
3414, 18, 31, 33syl3anc 1184 . 2
35 dihopelvalcp.p . . . . . . . . 9
36 dihopelvalcp.t . . . . . . . . 9
37 dihopelvalcp.e . . . . . . . . 9
38 dihopelvalcp.g . . . . . . . . 9
39 vex 2951 . . . . . . . . 9
40 vex 2951 . . . . . . . . 9
412, 5, 6, 35, 36, 37, 9, 38, 39, 40dicopelval2 31880 . . . . . . . 8
4214, 15, 41syl2anc 643 . . . . . . 7
43 dihopelvalcp.r . . . . . . . . 9
44 dihopelvalcp.z . . . . . . . . 9
451, 2, 6, 36, 43, 44, 8dibopelval3 31847 . . . . . . . 8
4614, 27, 29, 45syl12anc 1182 . . . . . . 7
4742, 46anbi12d 692 . . . . . 6
4847anbi1d 686 . . . . 5
49 simpl1 960 . . . . . . . . . . 11
50 simprll 739 . . . . . . . . . . . 12
51 simprlr 740 . . . . . . . . . . . . 13
522, 5, 6, 35lhpocnel2 30717 . . . . . . . . . . . . . . 15
5349, 52syl 16 . . . . . . . . . . . . . 14
54 simpl3l 1012 . . . . . . . . . . . . . 14
552, 5, 6, 36, 38ltrniotacl 31277 . . . . . . . . . . . . . 14
5649, 53, 54, 55syl3anc 1184 . . . . . . . . . . . . 13
576, 36, 37tendocl 31465 . . . . . . . . . . . . 13
5849, 51, 56, 57syl3anc 1184 . . . . . . . . . . . 12
5950, 58eqeltrd 2509 . . . . . . . . . . 11
60 simprll 739 . . . . . . . . . . . 12
6160adantl 453 . . . . . . . . . . 11
62 simprrr 742 . . . . . . . . . . . 12
631, 6, 36, 37, 44tendo0cl 31488 . . . . . . . . . . . . 13
6449, 63syl 16 . . . . . . . . . . . 12
6562, 64eqeltrd 2509 . . . . . . . . . . 11
66 eqid 2435 . . . . . . . . . . . 12 Scalar Scalar
67 eqid 2435 . . . . . . . . . . . 12 Scalar Scalar
686, 36, 37, 10, 66, 32, 67dvhopvadd 31792 . . . . . . . . . . 11 Scalar
6949, 59, 51, 61, 65, 68syl122anc 1193 . . . . . . . . . 10 Scalar
70 dihopelvalcp.o . . . . . . . . . . . . . 14
716, 36, 37, 10, 66, 70, 67dvhfplusr 31783 . . . . . . . . . . . . 13 Scalar
7249, 71syl 16 . . . . . . . . . . . 12 Scalar
7372oveqd 6090 . . . . . . . . . . 11 Scalar
7473opeq2d 3983 . . . . . . . . . 10 Scalar
7569, 74eqtrd 2467 . . . . . . . . 9
7675eqeq2d 2446 . . . . . . . 8
77 dihopelvalcp.f . . . . . . . . . 10
78 dihopelvalcp.s . . . . . . . . . 10
7977, 78opth 4427 . . . . . . . . 9
8062oveq2d 6089 . . . . . . . . . . . 12
811, 6, 36, 37, 44, 70tendo0plr 31490 . . . . . . . . . . . . 13
8249, 51, 81syl2anc 643 . . . . . . . . . . . 12
8380, 82eqtrd 2467 . . . . . . . . . . 11
8483eqeq2d 2446 . . . . . . . . . 10
8584anbi2d 685 . . . . . . . . 9
8679, 85syl5bb 249 . . . . . . . 8
8776, 86bitrd 245 . . . . . . 7
8887pm5.32da 623 . . . . . 6
89 simplll 735 . . . . . . . . . . 11
9089adantl 453 . . . . . . . . . 10
91 simprrr 742 . . . . . . . . . . 11
9291fveq1d 5722 . . . . . . . . . 10
9390, 92eqtr4d 2470 . . . . . . . . 9
9491eqcomd 2440 . . . . . . . . 9
95 coass 5380 . . . . . . . . . . 11
96 simpl1 960 . . . . . . . . . . . . . . 15
97 simpllr 736 . . . . . . . . . . . . . . . . . 18
9897adantl 453 . . . . . . . . . . . . . . . . 17
9991, 98eqeltrd 2509 . . . . . . . . . . . . . . . 16
10056adantrr 698 . . . . . . . . . . . . . . . 16
1016, 36, 37tendocl 31465 . . . . . . . . . . . . . . . 16
10296, 99, 100, 101syl3anc 1184 . . . . . . . . . . . . . . 15
1031, 6, 36ltrn1o 30822 . . . . . . . . . . . . . . 15
10496, 102, 103syl2anc 643 . . . . . . . . . . . . . 14
105 f1ococnv1 5696 . . . . . . . . . . . . . 14
106104, 105syl 16 . . . . . . . . . . . . 13
107106coeq1d 5026 . . . . . . . . . . . 12
10860ad2antrl 709 . . . . . . . . . . . . . 14
1091, 6, 36ltrn1o 30822 . . . . . . . . . . . . . 14
11096, 108, 109syl2anc 643 . . . . . . . . . . . . 13
111 f1of 5666 . . . . . . . . . . . . 13
112 fcoi2 5610 . . . . . . . . . . . . 13
113110, 111, 1123syl 19 . . . . . . . . . . . 12
114107, 113eqtr2d 2468 . . . . . . . . . . 11
115 simprrl 741 . . . . . . . . . . . . . 14
11693coeq1d 5026 . . . . . . . . . . . . . 14
117115, 116eqtrd 2467 . . . . . . . . . . . . 13
118117coeq1d 5026 . . . . . . . . . . . 12
1196, 36ltrncnv 30844 . . . . . . . . . . . . . 14
12096, 102, 119syl2anc 643 . . . . . . . . . . . . 13
1216, 36ltrnco 31417 . . . . . . . . . . . . . 14
12296, 102, 108, 121syl3anc 1184 . . . . . . . . . . . . 13
1236, 36ltrncom 31436 . . . . . . . . . . . . 13
12496, 120, 122, 123syl3anc 1184 . . . . . . . . . . . 12
125118, 124eqtr4d 2470 . . . . . . . . . . 11
12695, 114, 1253eqtr4a 2493 . . . . . . . . . 10
127 simplrr 738 . . . . . . . . . . 11
128127adantl 453 . . . . . . . . . 10
129126, 128jca 519 . . . . . . . . 9
13093, 94, 129jca31 521 . . . . . . . 8
131130ex 424 . . . . . . 7
132131pm4.71rd 617 . . . . . 6
13388, 132bitrd 245 . . . . 5
134 simprrl 741 . . . . . . . . . 10
135 simpll1 996 . . . . . . . . . . 11
13689adantl 453 . . . . . . . . . . . 12
13797adantl 453 . . . . . . . . . . . . 13
138135, 52syl 16 . . . . . . . . . . . . . 14
139 simpl3l 1012 . . . . . . . . . . . . . . 15
140139adantr 452 . . . . . . . . . . . . . 14
141135, 138, 140, 55syl3anc 1184 . . . . . . . . . . . . 13
142135, 137, 141, 57syl3anc 1184 . . . . . . . . . . . 12
143136, 142eqeltrd 2509 . . . . . . . . . . 11
14460ad2antrl 709 . . . . . . . . . . 11
1456, 36ltrnco 31417 . . . . . . . . . . 11
146135, 143, 144, 145syl3anc 1184 . . . . . . . . . 10
147134, 146eqeltrd 2509 . . . . . . . . 9
148 simpl1l 1008 . . . . . . . . . . . 12
149148adantr 452 . . . . . . . . . . 11
150149, 20syl 16 . . . . . . . . . 10
1511, 6, 36, 43trlcl 30862 . . . . . . . . . . 11
152135, 144, 151syl2anc 643 . . . . . . . . . 10
153 simpl2l 1010 . . . . . . . . . . . 12
154153adantr 452 . . . . . . . . . . 11
155 simpl1r 1009 . . . . . . . . . . . . 13
156155adantr 452 . . . . . . . . . . . 12
157156, 24syl 16 . . . . . . . . . . 11
158150, 154, 157, 26syl3anc 1184 . . . . . . . . . 10
159 simprlr 740 . . . . . . . . . . 11
160159ad2antrl 709 . . . . . . . . . 10
1611, 2, 4latmle1 14495 . . . . . . . . . . 11
162150, 154, 157, 161syl3anc 1184 . . . . . . . . . 10
1631, 2, 150, 152, 158, 154, 160, 162lattrd 14477 . . . . . . . . 9
164147, 137, 163jca31 521 . . . . . . . 8
165 simprll 739 . . . . . . . . . . . 12
166165adantr 452 . . . . . . . . . . 11
167 simprlr 740 . . . . . . . . . . . . 13
168167adantr 452 . . . . . . . . . . . 12
169168fveq1d 5722 . . . . . . . . . . 11
170166, 169eqtr4d 2470 . . . . . . . . . 10
171 simprlr 740 . . . . . . . . . 10
172170, 171jca 519 . . . . . . . . 9
173 simprrl 741 . . . . . . . . . . . 12
174173adantr 452 . . . . . . . . . . 11
175 simpll1 996 . . . . . . . . . . . 12
176 simprll 739 . . . . . . . . . . . 12
177168, 171eqeltrrd 2510 . . . . . . . . . . . . . 14
178175, 52syl 16 . . . . . . . . . . . . . . 15
179139adantr 452 . . . . . . . . . . . . . . 15
180175, 178, 179, 55syl3anc 1184 . . . . . . . . . . . . . 14
181175, 177, 180, 101syl3anc 1184 . . . . . . . . . . . . 13
182175, 181, 119syl2anc 643 . . . . . . . . . . . 12
1836, 36ltrnco 31417 . . . . . . . . . . . 12
184175, 176, 182, 183syl3anc 1184 . . . . . . . . . . 11
185174, 184eqeltrd 2509 . . . . . . . . . 10
186 simprr 734 . . . . . . . . . . 11
1872, 6, 36, 43trlle 30882 . . . . . . . . . . . 12
188175, 185, 187syl2anc 643 . . . . . . . . . . 11
189148adantr 452 . . . . . . . . . . . . 13