ltrncnv - Mathbox for Norm Megill

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

Theorem ltrncnv 34817

Description: The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.)

**Hypotheses**
Ref	Expression
ltrncnv.h
ltrncnv.t

**Assertion**
Ref	Expression
ltrncnv	$/\$ $/\$

Proof of Theorem ltrncnv Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrncnv.h	. . . 4
2		eqid 2460	. . . 4
3		ltrncnv.t	. . . 4
4	1, 2, 3	ltrnldil 34793	. . 3 $/\$ $/\$
5	1, 2	ldilcnv 34786	. . 3 $/\$ $/\$
6	4, 5	syldan 470	. 2 $/\$ $/\$
7		simp1 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simp1l 1015	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		simp1r 1016	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simp2l 1017	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp3l 1019	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2460	. . . . . . . 8
13		eqid 2460	. . . . . . . 8
14	12, 13, 1, 3	ltrncnvel 34813	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	8, 9, 10, 11, 14	syl112anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp2r 1018	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp3r 1020	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	12, 13, 1, 3	ltrncnvel 34813	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
19	8, 9, 16, 17, 18	syl112anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqid 2460	. . . . . . 7
21		eqid 2460	. . . . . . 7
22	12, 20, 21, 13, 1, 3	ltrnu 34792	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23	7, 15, 19, 22	syl3anc 1223	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		eqid 2460	. . . . . . . . . . 11
25	24, 1, 3	ltrn1o 34795	. . . . . . . . . 10 $/\$ $/\$
26	25	3ad2ant1 1012	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	24, 13	atbase 33961	. . . . . . . . . 10
28	10, 27	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		f1ocnvfv2 6162	. . . . . . . . 9 $/\$
30	26, 28, 29	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	30	oveq2d 6291	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp1ll 1054	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	12, 13, 1, 3	ltrncnvat 34812	. . . . . . . . 9 $/\$ $/\$ $/\$
34	8, 9, 10, 33	syl3anc 1223	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	20, 13	hlatjcom 34039	. . . . . . . 8 $/\$ $/\$
36	32, 34, 10, 35	syl3anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	31, 36	eqtrd 2501	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	oveq1d 6290	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	24, 13	atbase 33961	. . . . . . . . . 10
40	16, 39	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		f1ocnvfv2 6162	. . . . . . . . 9 $/\$
42	26, 40, 41	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	42	oveq2d 6291	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	12, 13, 1, 3	ltrncnvat 34812	. . . . . . . . 9 $/\$ $/\$ $/\$
45	8, 9, 16, 44	syl3anc 1223	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	20, 13	hlatjcom 34039	. . . . . . . 8 $/\$ $/\$
47	32, 45, 16, 46	syl3anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	43, 47	eqtrd 2501	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	oveq1d 6290	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	23, 38, 49	3eqtr3d 2509	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	3exp 1190	. . 3 $/\$ $/\$ $/\$ $/\$
52	51	ralrimivv 2877	. 2 $/\$ $/\$ $/\$
53	12, 20, 21, 13, 1, 2, 3	isltrn 34790	. . 3 $/\$ $/\$ $/\$
54	53	adantr 465	. 2 $/\$ $/\$ $/\$ $/\$
55	6, 52, 54	mpbir2and 915	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1374

wcel 1762

wral 2807 class class class wbr 4440

ccnv 4991

wf1o 5578

cfv 5579 (class class class)co 6275

cbs 14479

cple 14551

cjn 15420

cmee 15421

catm 33935

chlt 34022

clh 34655

cldil 34771

cltrn 34772

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-op 4027 df-uni 4239 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-id 4788 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-map 7412 df-poset 15422 df-plt 15434 df-lub 15450 df-glb 15451 df-join 15452 df-p0 15515 df-lat 15522 df-oposet 33848 df-ol 33850 df-oml 33851 df-covers 33938 df-ats 33939 df-atl 33970 df-cvlat 33994 df-hlat 34023 df-lhyp 34659 df-laut 34660 df-ldil 34775 df-ltrn 34776

This theorem is referenced by: trlcnv 34836 trlcocnv 35391 trlcoabs2N 35393 trlcoat 35394 trlcocnvat 35395 trlcone 35399 cdlemg46 35406 tgrpgrplem 35420 tendoicl 35467 cdlemh1 35486 cdlemh2 35487 cdlemh 35488 cdlemi2 35490 cdlemi 35491 cdlemk2 35503 cdlemk3 35504 cdlemk4 35505 cdlemk8 35509 cdlemk9 35510 cdlemk9bN 35511 cdlemkvcl 35513 cdlemk10 35514 cdlemk11 35520 cdlemk12 35521 cdlemk14 35525 cdlemk11u 35542 cdlemk12u 35543 cdlemk37 35585 cdlemkfid1N 35592 cdlemkid1 35593 cdlemkid2 35595 tendocnv 35693 tendospcanN 35695 dvhgrp 35779 cdlemn8 35876 dihopelvalcpre 35920 dih1 35958 dihglbcpreN 35972 dihjatcclem3 36092 dihjatcclem4 36093

W3C validator