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 35325

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 1107	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simp12l 1109	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simp13l 1111	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		simp21 1029	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
5		cdlemef46g.j	. . . 4 $.\/$
6		cdlemef46g.a	. . . 4
7		eqid 2467	. . . 4
8	5, 6, 7	llni2 34308	. . 3 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1231	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10		simp1 996	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp23 1031	. . . . 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 35312	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	10, 11, 4, 24	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
26	25	simpld 459	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
27		simp11 1026	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
28		simp22 1030	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
29	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fvaw 35297	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	10, 28, 29	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
31		simp23l 1117	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32		simp3l 1024	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
33	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fsvlpq 35301	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
34	10, 4, 28, 32, 33	syl121anc 1233	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35		simp3r 1025	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
36		nbrne2 4465	. . . . 5 $.\/$ $/\$ $.\/$
37	34, 35, 36	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
38		cdlemeg46.x	. . . . 5 $.\/$ $./\$
39	13, 5, 14, 6, 15, 38	lhpat2 34841	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	27, 30, 31, 37, 39	syl112anc 1232	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		hllat 34160	. . . . . . . 8
42	1, 41	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
43	30	simpld 459	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
44	12, 5, 6	hlatjcl 34163	. . . . . . . 8 $/\$ $/\$ $.\/$
45	1, 43, 31, 44	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46		simp11r 1108	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	12, 15	lhpbase 34794	. . . . . . . 8
48	46, 47	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
49	12, 13, 14	latmle2 15560	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
50	42, 45, 48, 49	syl3anc 1228	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
51	38, 50	syl5eqbr 4480	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	25	simprd 463	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
53		nbrne2 4465	. . . . 5 $/\$
54	51, 52, 53	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
55	54	necomd 2738	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	5, 6, 7	llni2 34308	. . 3 $/\$ $/\$ $/\$ $.\/$
57	1, 26, 40, 55, 56	syl31anc 1231	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
58		simp22l 1115	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
59	13, 5, 6	hlatlej1 34171	. . . . 5 $/\$ $/\$ $.\/$
60	1, 26, 40, 59	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
61	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdlemeg46nlpq 35313	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	10, 4, 11, 35, 61	syl121anc 1233	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
63		nbrne1 4464	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
64	60, 62, 63	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
65	64	necomd 2738	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
66		cdlemeg46.y	. . . 4 $.\/$ $./\$
67	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38	cdlemeg46rgv 35324	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
68	12, 6	atbase 34086	. . . . 5
69	58, 68	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70	12, 5, 6	hlatjcl 34163	. . . . 5 $/\$ $/\$ $.\/$
71	1, 2, 3, 70	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
72	12, 5, 6	hlatjcl 34163	. . . . 5 $/\$ $/\$ $.\/$
73	1, 26, 40, 72	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
74	12, 13, 14	latlem12 15561	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
75	42, 69, 71, 73, 74	syl13anc 1230	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
76	32, 67, 75	mpbi2and 919	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
77	13, 14, 6, 7	2llnmeqat 34367	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	1, 9, 57, 58, 65, 76, 77	syl132anc 1246	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662

wral 2814

csb 3435

cif 3939 class class class wbr 4447

cmpt 4505

cfv 5586

crio 6242 (class class class)co 6282

cbs 14486

cple 14558

cjn 15427

cmee 15428

clat 15528

catm 34060

chlt 34147

clln 34287

clh 34780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-riotaBAD 33756

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-1st 6781 df-2nd 6782 df-undef 6999 df-poset 15429 df-plt 15441 df-lub 15457 df-glb 15458 df-join 15459 df-meet 15460 df-p0 15522 df-p1 15523 df-lat 15529 df-clat 15591 df-oposet 33973 df-ol 33975 df-oml 33976 df-covers 34063 df-ats 34064 df-atl 34095 df-cvlat 34119 df-hlat 34148 df-llines 34294 df-lplanes 34295 df-lvols 34296 df-lines 34297 df-psubsp 34299 df-pmap 34300 df-padd 34592 df-lhyp 34784

This theorem is referenced by: cdlemeg46gfr 35327

W3C validator