mod1ile - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mod1ile		Structured version Unicode version

Theorem mod1ile 15604

Description: The weak direction of the modular law (e.g. pmod1i 35274, atmod1i1 35283) that holds in any lattice. (Contributed by NM, 11-May-2012.)

**Hypotheses**
Ref	Expression
modle.b
modle.l
modle.j	$.\/$
modle.m	$./\$

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

**Proof of Theorem mod1ile**
Step	Hyp	Ref	Expression
1		simpll 753	. . . . 5 $/\$ $/\$ $/\$ $/\$
2		simplr1 1037	. . . . 5 $/\$ $/\$ $/\$ $/\$
3		simplr2 1038	. . . . 5 $/\$ $/\$ $/\$ $/\$
4		modle.b	. . . . . 6
5		modle.l	. . . . . 6
6		modle.j	. . . . . 6 $.\/$
7	4, 5, 6	latlej1 15559	. . . . 5 $/\$ $/\$ $.\/$
8	1, 2, 3, 7	syl3anc 1227	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
9		simpr 461	. . . 4 $/\$ $/\$ $/\$ $/\$
10	4, 6	latjcl 15550	. . . . . 6 $/\$ $/\$ $.\/$
11	1, 2, 3, 10	syl3anc 1227	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
12		simplr3 1039	. . . . 5 $/\$ $/\$ $/\$ $/\$
13		modle.m	. . . . . 6 $./\$
14	4, 5, 13	latlem12 15577	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$
15	1, 2, 11, 12, 14	syl13anc 1229	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
16	8, 9, 15	mpbi2and 919	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
17	4, 5, 6, 13	latmlej12 15590	. . . . 5 $/\$ $/\$ $/\$ $./\$ $.\/$
18	1, 3, 12, 2, 17	syl13anc 1229	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$
19	4, 5, 13	latmle2 15576	. . . . 5 $/\$ $/\$ $./\$
20	1, 3, 12, 19	syl3anc 1227	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$
21	4, 13	latmcl 15551	. . . . . 6 $/\$ $/\$ $./\$
22	1, 3, 12, 21	syl3anc 1227	. . . . 5 $/\$ $/\$ $/\$ $/\$ $./\$
23	4, 5, 13	latlem12 15577	. . . . 5 $/\$ $./\$ $/\$ $.\/$ $/\$ $./\$ $.\/$ $/\$ $./\$ $./\$ $.\/$ $./\$
24	1, 22, 11, 12, 23	syl13anc 1229	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$ $/\$ $./\$ $./\$ $.\/$ $./\$
25	18, 20, 24	mpbi2and 919	. . 3 $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$
26	4, 13	latmcl 15551	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $./\$
27	1, 11, 12, 26	syl3anc 1227	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
28	4, 5, 6	latjle12 15561	. . . 4 $/\$ $/\$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
29	1, 2, 22, 27, 28	syl13anc 1229	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
30	16, 25, 29	mpbi2and 919	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
31	30	ex 434	1 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1381

wcel 1802 class class class wbr 4433

cfv 5574 (class class class)co 6277

cbs 14504

cple 14576

cjn 15442

cmee 15443

clat 15544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-ral 2796 df-rex 2797 df-reu 2798 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-op 4017 df-uni 4231 df-iun 4313 df-br 4434 df-opab 4492 df-mpt 4493 df-id 4781 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-riota 6238 df-ov 6280 df-oprab 6281 df-poset 15444 df-lub 15473 df-glb 15474 df-join 15475 df-meet 15476 df-lat 15545

This theorem is referenced by: mod2ile 15605 hlmod1i 35282

W3C validator