cdlemeg46req - Mathbox for Norm Megill

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

Theorem cdlemeg46req 34108

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 1120	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simp12l 1122	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simp13l 1124	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		simp21 1042	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
5		cdlemef46g.j	. . . 4 $.\/$
6		cdlemef46g.a	. . . 4
7		eqid 2453	. . . 4
8	5, 6, 7	llni2 33089	. . 3 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1272	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10		simp1 1009	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp23 1044	. . . . 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 34095	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	10, 11, 4, 24	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
26	25	simpld 461	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
27		simp11 1039	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
28		simp22 1043	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
29	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fvaw 34080	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	10, 28, 29	syl2anc 667	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
31		simp23l 1130	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32		simp3l 1037	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
33	12, 13, 5, 14, 6, 15, 16, 17, 18, 19	cdleme46fsvlpq 34084	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
34	10, 4, 28, 32, 33	syl121anc 1274	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35		simp3r 1038	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
36		nbrne2 4424	. . . . 5 $.\/$ $/\$ $.\/$
37	34, 35, 36	syl2anc 667	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
38		cdlemeg46.x	. . . . 5 $.\/$ $./\$
39	13, 5, 14, 6, 15, 38	lhpat2 33622	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	27, 30, 31, 37, 39	syl112anc 1273	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		hllat 32941	. . . . . . . 8
42	1, 41	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
43	30	simpld 461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
44	12, 5, 6	hlatjcl 32944	. . . . . . . 8 $/\$ $/\$ $.\/$
45	1, 43, 31, 44	syl3anc 1269	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46		simp11r 1121	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	12, 15	lhpbase 33575	. . . . . . . 8
48	46, 47	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
49	12, 13, 14	latmle2 16335	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
50	42, 45, 48, 49	syl3anc 1269	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
51	38, 50	syl5eqbr 4439	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	25	simprd 465	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
53		nbrne2 4424	. . . . 5 $/\$
54	51, 52, 53	syl2anc 667	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
55	54	necomd 2681	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	5, 6, 7	llni2 33089	. . 3 $/\$ $/\$ $/\$ $.\/$
57	1, 26, 40, 55, 56	syl31anc 1272	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
58		simp22l 1128	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
59	13, 5, 6	hlatlej1 32952	. . . . 5 $/\$ $/\$ $.\/$
60	1, 26, 40, 59	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
61	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23	cdlemeg46nlpq 34096	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	10, 4, 11, 35, 61	syl121anc 1274	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
63		nbrne1 4423	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
64	60, 62, 63	syl2anc 667	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
65	64	necomd 2681	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
66		cdlemeg46.y	. . . 4 $.\/$ $./\$
67	12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38	cdlemeg46rgv 34107	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
68	12, 6	atbase 32867	. . . . 5
69	58, 68	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70	12, 5, 6	hlatjcl 32944	. . . . 5 $/\$ $/\$ $.\/$
71	1, 2, 3, 70	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
72	12, 5, 6	hlatjcl 32944	. . . . 5 $/\$ $/\$ $.\/$
73	1, 26, 40, 72	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
74	12, 13, 14	latlem12 16336	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
75	42, 69, 71, 73, 74	syl13anc 1271	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
76	32, 67, 75	mpbi2and 933	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
77	13, 14, 6, 7	2llnmeqat 33148	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
78	1, 9, 57, 58, 65, 76, 77	syl132anc 1287	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

wne 2624

wral 2739

csb 3365

cif 3883 class class class wbr 4405

cmpt 4464

cfv 5585

crio 6256 (class class class)co 6295

cbs 15133

cple 15209

cjn 16201

cmee 16202

clat 16303

catm 32841

chlt 32928

clln 33068

clh 33561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-riotaBAD 32537

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-iun 4283 df-iin 4284 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-1st 6798 df-2nd 6799 df-undef 7025 df-preset 16185 df-poset 16203 df-plt 16216 df-lub 16232 df-glb 16233 df-join 16234 df-meet 16235 df-p0 16297 df-p1 16298 df-lat 16304 df-clat 16366 df-oposet 32754 df-ol 32756 df-oml 32757 df-covers 32844 df-ats 32845 df-atl 32876 df-cvlat 32900 df-hlat 32929 df-llines 33075 df-lplanes 33076 df-lvols 33077 df-lines 33078 df-psubsp 33080 df-pmap 33081 df-padd 33373 df-lhyp 33565

This theorem is referenced by: cdlemeg46gfr 34110

W3C validator