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 36668

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 1105	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simp12l 1107	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simp13l 1109	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		simp21 1027	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
5		cdlemef46g.j	. . . 4 $.\/$
6		cdlemef46g.a	. . . 4
7		eqid 2382	. . . 4
8	5, 6, 7	llni2 35649	. . 3 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1229	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10		simp1 994	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp23 1029	. . . . 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 36655	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	10, 11, 4, 24	syl3anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
26	25	simpld 457	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
27		simp11 1024	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
28		simp22 1028	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
29	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fvaw 36640	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	10, 28, 29	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
31		simp23l 1115	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32		simp3l 1022	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
33	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fsvlpq 36644	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
34	10, 4, 28, 32, 33	syl121anc 1231	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35		simp3r 1023	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
36		nbrne2 4385	. . . . 5 $.\/$ $/\$ $.\/$
37	34, 35, 36	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
38		cdlemeg46.x	. . . . 5 $.\/$ $./\$
39	13, 5, 14, 6, 15, 38	lhpat2 36182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	27, 30, 31, 37, 39	syl112anc 1230	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		hllat 35501	. . . . . . . 8
42	1, 41	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
43	30	simpld 457	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
44	12, 5, 6	hlatjcl 35504	. . . . . . . 8 $/\$ $/\$ $.\/$
45	1, 43, 31, 44	syl3anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46		simp11r 1106	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	12, 15	lhpbase 36135	. . . . . . . 8
48	46, 47	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
49	12, 13, 14	latmle2 15824	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
50	42, 45, 48, 49	syl3anc 1226	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
51	38, 50	syl5eqbr 4400	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	25	simprd 461	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
53		nbrne2 4385	. . . . 5 $/\$
54	51, 52, 53	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
55	54	necomd 2653	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	5, 6, 7	llni2 35649	. . 3 $/\$ $/\$ $/\$ $.\/$
57	1, 26, 40, 55, 56	syl31anc 1229	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
58		simp22l 1113	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
59	13, 5, 6	hlatlej1 35512	. . . . 5 $/\$ $/\$ $.\/$
60	1, 26, 40, 59	syl3anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
61	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdlemeg46nlpq 36656	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	10, 4, 11, 35, 61	syl121anc 1231	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
63		nbrne1 4384	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
64	60, 62, 63	syl2anc 659	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
65	64	necomd 2653	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
66		cdlemeg46.y	. . . 4 $.\/$ $./\$
67	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38	cdlemeg46rgv 36667	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
68	12, 6	atbase 35427	. . . . 5
69	58, 68	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70	12, 5, 6	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
71	1, 2, 3, 70	syl3anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
72	12, 5, 6	hlatjcl 35504	. . . . 5 $/\$ $/\$ $.\/$
73	1, 26, 40, 72	syl3anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
74	12, 13, 14	latlem12 15825	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
75	42, 69, 71, 73, 74	syl13anc 1228	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
76	32, 67, 75	mpbi2and 919	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
77	13, 14, 6, 7	2llnmeqat 35708	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	1, 9, 57, 58, 65, 76, 77	syl132anc 1244	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wne 2577

wral 2732

csb 3348

cif 3857 class class class wbr 4367

cmpt 4425

cfv 5496

crio 6157 (class class class)co 6196

cbs 14634

cple 14709

cjn 15690

cmee 15691

clat 15792

catm 35401

chlt 35488

clln 35628

clh 36121

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-riotaBAD 35097

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-iin 4246 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-1st 6699 df-2nd 6700 df-undef 6920 df-preset 15674 df-poset 15692 df-plt 15705 df-lub 15721 df-glb 15722 df-join 15723 df-meet 15724 df-p0 15786 df-p1 15787 df-lat 15793 df-clat 15855 df-oposet 35314 df-ol 35316 df-oml 35317 df-covers 35404 df-ats 35405 df-atl 35436 df-cvlat 35460 df-hlat 35489 df-llines 35635 df-lplanes 35636 df-lvols 35637 df-lines 35638 df-psubsp 35640 df-pmap 35641 df-padd 35933 df-lhyp 36125

This theorem is referenced by: cdlemeg46gfr 36670

W3C validator