cdlemeg46req - Mathbox for Norm Megill

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

Theorem cdlemeg46req 34455

Description: TODO FIX COMMENT r = (v₁ $\/$ g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

**Hypotheses**
Ref	Expression
cdlemef46g.b
cdlemef46g.l
cdlemef46g.j	$.\/$
cdlemef46g.m	$./\$
cdlemef46g.a
cdlemef46g.h
cdlemef46g.u	$.\/$ $./\$
cdlemef46g.d	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemefs46g.e	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemef46g.f	$/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
cdlemef46.v	$.\/$ $./\$
cdlemef46.n	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemefs46.o	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemef46.g	$/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
cdlemeg46.y	$.\/$ $./\$
cdlemeg46.x	$.\/$ $./\$

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

Distinct variable groups:

$.\/$ ,

$./\$ ,

$.\/$ ,

$./\$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem cdlemeg46req**
Step	Hyp	Ref	Expression
1		simp11l 1099	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simp12l 1101	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simp13l 1103	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		simp21 1021	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
5		cdlemef46g.j	. . . 4 $.\/$
6		cdlemef46g.a	. . . 4
7		eqid 2450	. . . 4
8	5, 6, 7	llni2 33438	. . 3 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1222	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10		simp1 988	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp23 1023	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
12		cdlemef46g.b	. . . . . 6
13		cdlemef46g.l	. . . . . 6
14		cdlemef46g.m	. . . . . 6 $./\$
15		cdlemef46g.h	. . . . . 6
16		cdlemef46g.u	. . . . . 6 $.\/$ $./\$
17		cdlemef46g.d	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
18		cdlemefs46g.e	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
19		cdlemef46g.f	. . . . . 6 $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
20		cdlemef46.v	. . . . . 6 $.\/$ $./\$
21		cdlemef46.n	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22		cdlemefs46.o	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
23		cdlemef46.g	. . . . . 6 $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
24	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdlemeg46fvaw 34442	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	10, 11, 4, 24	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
26	25	simpld 459	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
27		simp11 1018	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
28		simp22 1022	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
29	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fvaw 34427	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	10, 28, 29	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
31		simp23l 1109	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32		simp3l 1016	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
33	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fsvlpq 34431	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
34	10, 4, 28, 32, 33	syl121anc 1224	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35		simp3r 1017	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
36		nbrne2 4394	. . . . 5 $.\/$ $/\$ $.\/$
37	34, 35, 36	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
38		cdlemeg46.x	. . . . 5 $.\/$ $./\$
39	13, 5, 14, 6, 15, 38	lhpat2 33971	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	27, 30, 31, 37, 39	syl112anc 1223	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		hllat 33290	. . . . . . . 8
42	1, 41	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
43	30	simpld 459	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
44	12, 5, 6	hlatjcl 33293	. . . . . . . 8 $/\$ $/\$ $.\/$
45	1, 43, 31, 44	syl3anc 1219	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46		simp11r 1100	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	12, 15	lhpbase 33924	. . . . . . . 8
48	46, 47	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
49	12, 13, 14	latmle2 15335	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
50	42, 45, 48, 49	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
51	38, 50	syl5eqbr 4409	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	25	simprd 463	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
53		nbrne2 4394	. . . . 5 $/\$
54	51, 52, 53	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
55	54	necomd 2716	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	5, 6, 7	llni2 33438	. . 3 $/\$ $/\$ $/\$ $.\/$
57	1, 26, 40, 55, 56	syl31anc 1222	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
58		simp22l 1107	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
59	13, 5, 6	hlatlej1 33301	. . . . 5 $/\$ $/\$ $.\/$
60	1, 26, 40, 59	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
61	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdlemeg46nlpq 34443	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	10, 4, 11, 35, 61	syl121anc 1224	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
63		nbrne1 4393	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
64	60, 62, 63	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
65	64	necomd 2716	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
66		cdlemeg46.y	. . . 4 $.\/$ $./\$
67	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38	cdlemeg46rgv 34454	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
68	12, 6	atbase 33216	. . . . 5
69	58, 68	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70	12, 5, 6	hlatjcl 33293	. . . . 5 $/\$ $/\$ $.\/$
71	1, 2, 3, 70	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
72	12, 5, 6	hlatjcl 33293	. . . . 5 $/\$ $/\$ $.\/$
73	1, 26, 40, 72	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
74	12, 13, 14	latlem12 15336	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
75	42, 69, 71, 73, 74	syl13anc 1221	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
76	32, 67, 75	mpbi2and 912	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
77	13, 14, 6, 7	2llnmeqat 33497	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	1, 9, 57, 58, 65, 76, 77	syl132anc 1237	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1757

wne 2641

wral 2792

csb 3372

cif 3875 class class class wbr 4376

cmpt 4434

cfv 5502

crio 6136 (class class class)co 6176

cbs 14262

cple 14333

cjn 15202

cmee 15203

clat 15303

catm 33190

chlt 33277

clln 33417

clh 33910

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 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-rep 4487 ax-sep 4497 ax-nul 4505 ax-pow 4554 ax-pr 4615 ax-un 6458 ax-riotaBAD 32886

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-nel 2644 df-ral 2797 df-rex 2798 df-reu 2799 df-rmo 2800 df-rab 2801 df-v 3056 df-sbc 3271 df-csb 3373 df-dif 3415 df-un 3417 df-in 3419 df-ss 3426 df-nul 3722 df-if 3876 df-pw 3946 df-sn 3962 df-pr 3964 df-op 3968 df-uni 4176 df-iun 4257 df-iin 4258 df-br 4377 df-opab 4435 df-mpt 4436 df-id 4720 df-xp 4930 df-rel 4931 df-cnv 4932 df-co 4933 df-dm 4934 df-rn 4935 df-res 4936 df-ima 4937 df-iota 5465 df-fun 5504 df-fn 5505 df-f 5506 df-f1 5507 df-fo 5508 df-f1o 5509 df-fv 5510 df-riota 6137 df-ov 6179 df-oprab 6180 df-mpt2 6181 df-1st 6663 df-2nd 6664 df-undef 6878 df-poset 15204 df-plt 15216 df-lub 15232 df-glb 15233 df-join 15234 df-meet 15235 df-p0 15297 df-p1 15298 df-lat 15304 df-clat 15366 df-oposet 33103 df-ol 33105 df-oml 33106 df-covers 33193 df-ats 33194 df-atl 33225 df-cvlat 33249 df-hlat 33278 df-llines 33424 df-lplanes 33425 df-lvols 33426 df-lines 33427 df-psubsp 33429 df-pmap 33430 df-padd 33722 df-lhyp 33914

This theorem is referenced by: cdlemeg46gfr 34457

W3C validator