cdlemd2 - Mathbox for Norm Megill

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

Theorem cdlemd2 34182

Description: Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.)

**Hypotheses**
Ref	Expression
cdlemd2.l
cdlemd2.j	$.\/$
cdlemd2.a
cdlemd2.h
cdlemd2.t

**Assertion**
Ref	Expression
cdlemd2	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$

**Proof of Theorem cdlemd2**
Step	Hyp	Ref	Expression
1		simp3l 1016	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
2		simp11 1018	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
3		simp12l 1101	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp11l 1099	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		hllat 33347	. . . . . . . . . 10
6	4, 5	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
7		simp21l 1105	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
8		simp13 1020	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
9		eqid 2454	. . . . . . . . . . 11
10		cdlemd2.j	. . . . . . . . . . 11 $.\/$
11		cdlemd2.a	. . . . . . . . . . 11
12	9, 10, 11	hlatjcl 33350	. . . . . . . . . 10 $/\$ $/\$ $.\/$
13	4, 7, 8, 12	syl3anc 1219	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
14		simp11r 1100	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
15		cdlemd2.h	. . . . . . . . . . 11
16	9, 15	lhpbase 33981	. . . . . . . . . 10
17	14, 16	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
18		eqid 2454	. . . . . . . . . 10
19	9, 18	latmcl 15342	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$
20	6, 13, 17, 19	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
21		cdlemd2.l	. . . . . . . . . 10
22	9, 21, 18	latmle2 15367	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$
23	6, 13, 17, 22	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
24		cdlemd2.t	. . . . . . . . 9
25	9, 21, 15, 24	ltrnval1 34117	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
26	2, 3, 20, 23, 25	syl112anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
27		simp12r 1102	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
28	9, 21, 15, 24	ltrnval1 34117	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
29	2, 27, 20, 23, 28	syl112anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
30	26, 29	eqtr4d 2498	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
31	1, 30	oveq12d 6219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
32	9, 11	atbase 33273	. . . . . . 7
33	7, 32	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
34	9, 10, 15, 24	ltrnj 34115	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
35	2, 3, 33, 20, 34	syl112anc 1223	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
36	9, 10, 15, 24	ltrnj 34115	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
37	2, 27, 33, 20, 36	syl112anc 1223	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
38	31, 35, 37	3eqtr4d 2505	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
39		simp3r 1017	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
40		simp22l 1107	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
41	9, 10, 11	hlatjcl 33350	. . . . . . . . . 10 $/\$ $/\$ $.\/$
42	4, 40, 8, 41	syl3anc 1219	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
43	9, 18	latmcl 15342	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$
44	6, 42, 17, 43	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
45	9, 21, 18	latmle2 15367	. . . . . . . . 9 $/\$ $.\/$ $/\$ $.\/$
46	6, 42, 17, 45	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
47	9, 21, 15, 24	ltrnval1 34117	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	2, 3, 44, 46, 47	syl112anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
49	9, 21, 15, 24	ltrnval1 34117	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	2, 27, 44, 46, 49	syl112anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
51	48, 50	eqtr4d 2498	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
52	39, 51	oveq12d 6219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
53	9, 11	atbase 33273	. . . . . . 7
54	40, 53	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
55	9, 10, 15, 24	ltrnj 34115	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
56	2, 3, 54, 44, 55	syl112anc 1223	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
57	9, 10, 15, 24	ltrnj 34115	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
58	2, 27, 54, 44, 57	syl112anc 1223	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
59	52, 56, 58	3eqtr4d 2505	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
60	38, 59	oveq12d 6219	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
61	9, 10	latjcl 15341	. . . . 5 $/\$ $/\$ $.\/$ $.\/$ $.\/$
62	6, 33, 20, 61	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
63	9, 10	latjcl 15341	. . . . 5 $/\$ $/\$ $.\/$ $.\/$ $.\/$
64	6, 54, 44, 63	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
65	9, 18, 15, 24	ltrnm 34114	. . . 4 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
66	2, 3, 62, 64, 65	syl112anc 1223	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
67	9, 18, 15, 24	ltrnm 34114	. . . 4 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
68	2, 27, 62, 64, 67	syl112anc 1223	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
69	60, 66, 68	3eqtr4d 2505	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
70		simp21 1021	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
71		simp22 1022	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
72		simp23l 1109	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
73		simp23r 1110	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
74	8, 72, 73	3jca 1168	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
75	21, 10, 18, 11, 15	cdlemd1 34181	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
76	2, 70, 71, 74, 75	syl13anc 1221	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
77	76	fveq2d 5804	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
78	76	fveq2d 5804	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
79	69, 77, 78	3eqtr4d 2505	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2648 class class class wbr 4401

cfv 5527 (class class class)co 6201

cbs 14293

cple 14365

cjn 15234

cmee 15235

clat 15335

catm 33247

chlt 33334

clh 33967

cltrn 34084

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4512 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-iun 4282 df-iin 4283 df-br 4402 df-opab 4460 df-mpt 4461 df-id 4745 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-f1 5532 df-fo 5533 df-f1o 5534 df-fv 5535 df-riota 6162 df-ov 6204 df-oprab 6205 df-mpt2 6206 df-1st 6688 df-2nd 6689 df-map 7327 df-poset 15236 df-plt 15248 df-lub 15264 df-glb 15265 df-join 15266 df-meet 15267 df-p0 15329 df-p1 15330 df-lat 15336 df-clat 15398 df-oposet 33160 df-ol 33162 df-oml 33163 df-covers 33250 df-ats 33251 df-atl 33282 df-cvlat 33306 df-hlat 33335 df-psubsp 33486 df-pmap 33487 df-padd 33779 df-lhyp 33971 df-laut 33972 df-ldil 34087 df-ltrn 34088

This theorem is referenced by: cdlemd4 34184 cdlemd5 34185

W3C validator