ltrncnv - Mathbox for Norm Megill

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

Theorem ltrncnv 33782

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 2471	. . . 4
3		ltrncnv.t	. . . 4
4	1, 2, 3	ltrnldil 33758	. . 3 $/\$ $/\$
5	1, 2	ldilcnv 33751	. . 3 $/\$ $/\$
6	4, 5	syldan 478	. 2 $/\$ $/\$
7		simp1 1030	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simp1l 1054	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		simp1r 1055	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simp2l 1056	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp3l 1058	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2471	. . . . . . . 8
13		eqid 2471	. . . . . . . 8
14	12, 13, 1, 3	ltrncnvel 33778	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	8, 9, 10, 11, 14	syl112anc 1296	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp2r 1057	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp3r 1059	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	12, 13, 1, 3	ltrncnvel 33778	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
19	8, 9, 16, 17, 18	syl112anc 1296	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqid 2471	. . . . . . 7
21		eqid 2471	. . . . . . 7
22	12, 20, 21, 13, 1, 3	ltrnu 33757	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23	7, 15, 19, 22	syl3anc 1292	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		eqid 2471	. . . . . . . . . . 11
25	24, 1, 3	ltrn1o 33760	. . . . . . . . . 10 $/\$ $/\$
26	25	3ad2ant1 1051	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	24, 13	atbase 32926	. . . . . . . . . 10
28	10, 27	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		f1ocnvfv2 6194	. . . . . . . . 9 $/\$
30	26, 28, 29	syl2anc 673	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	30	oveq2d 6324	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp1ll 1093	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	12, 13, 1, 3	ltrncnvat 33777	. . . . . . . . 9 $/\$ $/\$ $/\$
34	8, 9, 10, 33	syl3anc 1292	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	20, 13	hlatjcom 33004	. . . . . . . 8 $/\$ $/\$
36	32, 34, 10, 35	syl3anc 1292	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	31, 36	eqtrd 2505	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	oveq1d 6323	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	24, 13	atbase 32926	. . . . . . . . . 10
40	16, 39	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		f1ocnvfv2 6194	. . . . . . . . 9 $/\$
42	26, 40, 41	syl2anc 673	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	42	oveq2d 6324	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	12, 13, 1, 3	ltrncnvat 33777	. . . . . . . . 9 $/\$ $/\$ $/\$
45	8, 9, 16, 44	syl3anc 1292	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	20, 13	hlatjcom 33004	. . . . . . . 8 $/\$ $/\$
47	32, 45, 16, 46	syl3anc 1292	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	43, 47	eqtrd 2505	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	oveq1d 6323	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	23, 38, 49	3eqtr3d 2513	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	3exp 1230	. . 3 $/\$ $/\$ $/\$ $/\$
52	51	ralrimivv 2813	. 2 $/\$ $/\$ $/\$
53	12, 20, 21, 13, 1, 2, 3	isltrn 33755	. . 3 $/\$ $/\$ $/\$
54	53	adantr 472	. 2 $/\$ $/\$ $/\$ $/\$
55	6, 52, 54	mpbir2and 936	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756 class class class wbr 4395

ccnv 4838

wf1o 5588

cfv 5589 (class class class)co 6308

cbs 15199

cple 15275

cjn 16267

cmee 16268

catm 32900

chlt 32987

clh 33620

cldil 33736

cltrn 33737

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-map 7492 df-preset 16251 df-poset 16269 df-plt 16282 df-lub 16298 df-glb 16299 df-join 16300 df-p0 16363 df-lat 16370 df-oposet 32813 df-ol 32815 df-oml 32816 df-covers 32903 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988 df-lhyp 33624 df-laut 33625 df-ldil 33740 df-ltrn 33741

This theorem is referenced by: trlcnv 33802 trlcocnv 34358 trlcoabs2N 34360 trlcoat 34361 trlcocnvat 34362 trlcone 34366 cdlemg46 34373 tgrpgrplem 34387 tendoicl 34434 cdlemh1 34453 cdlemh2 34454 cdlemh 34455 cdlemi2 34457 cdlemi 34458 cdlemk2 34470 cdlemk3 34471 cdlemk4 34472 cdlemk8 34476 cdlemk9 34477 cdlemk9bN 34478 cdlemkvcl 34480 cdlemk10 34481 cdlemk11 34487 cdlemk12 34488 cdlemk14 34492 cdlemk11u 34509 cdlemk12u 34510 cdlemk37 34552 cdlemkfid1N 34559 cdlemkid1 34560 cdlemkid2 34562 tendocnv 34660 tendospcanN 34662 dvhgrp 34746 cdlemn8 34843 dihopelvalcpre 34887 dih1 34925 dihglbcpreN 34939 dihjatcclem3 35059 dihjatcclem4 35060

W3C validator