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 33790

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 2443	. . . 4
3		ltrncnv.t	. . . 4
4	1, 2, 3	ltrnldil 33766	. . 3 $/\$ $/\$
5	1, 2	ldilcnv 33759	. . 3 $/\$ $/\$
6	4, 5	syldan 470	. 2 $/\$ $/\$
7		simp1 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simp1l 1012	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		simp1r 1013	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simp2l 1014	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp3l 1016	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2443	. . . . . . . 8
13		eqid 2443	. . . . . . . 8
14	12, 13, 1, 3	ltrncnvel 33786	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	8, 9, 10, 11, 14	syl112anc 1222	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp2r 1015	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp3r 1017	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	12, 13, 1, 3	ltrncnvel 33786	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
19	8, 9, 16, 17, 18	syl112anc 1222	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqid 2443	. . . . . . 7
21		eqid 2443	. . . . . . 7
22	12, 20, 21, 13, 1, 3	ltrnu 33765	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23	7, 15, 19, 22	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		eqid 2443	. . . . . . . . . . 11
25	24, 1, 3	ltrn1o 33768	. . . . . . . . . 10 $/\$ $/\$
26	25	3ad2ant1 1009	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	24, 13	atbase 32934	. . . . . . . . . 10
28	10, 27	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		f1ocnvfv2 5984	. . . . . . . . 9 $/\$
30	26, 28, 29	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	30	oveq2d 6107	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp1ll 1051	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	12, 13, 1, 3	ltrncnvat 33785	. . . . . . . . 9 $/\$ $/\$ $/\$
34	8, 9, 10, 33	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	20, 13	hlatjcom 33012	. . . . . . . 8 $/\$ $/\$
36	32, 34, 10, 35	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	31, 36	eqtrd 2475	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	oveq1d 6106	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	24, 13	atbase 32934	. . . . . . . . . 10
40	16, 39	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		f1ocnvfv2 5984	. . . . . . . . 9 $/\$
42	26, 40, 41	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	42	oveq2d 6107	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	12, 13, 1, 3	ltrncnvat 33785	. . . . . . . . 9 $/\$ $/\$ $/\$
45	8, 9, 16, 44	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	20, 13	hlatjcom 33012	. . . . . . . 8 $/\$ $/\$
47	32, 45, 16, 46	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	43, 47	eqtrd 2475	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	oveq1d 6106	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	23, 38, 49	3eqtr3d 2483	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	3exp 1186	. . 3 $/\$ $/\$ $/\$ $/\$
52	51	ralrimivv 2807	. 2 $/\$ $/\$ $/\$
53	12, 20, 21, 13, 1, 2, 3	isltrn 33763	. . 3 $/\$ $/\$ $/\$
54	53	adantr 465	. 2 $/\$ $/\$ $/\$ $/\$
55	6, 52, 54	mpbir2and 913	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wral 2715 class class class wbr 4292

ccnv 4839

wf1o 5417

cfv 5418 (class class class)co 6091

cbs 14174

cple 14245

cjn 15114

cmee 15115

catm 32908

chlt 32995

clh 33628

cldil 33744

cltrn 33745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-id 4636 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-map 7216 df-poset 15116 df-plt 15128 df-lub 15144 df-glb 15145 df-join 15146 df-p0 15209 df-lat 15216 df-oposet 32821 df-ol 32823 df-oml 32824 df-covers 32911 df-ats 32912 df-atl 32943 df-cvlat 32967 df-hlat 32996 df-lhyp 33632 df-laut 33633 df-ldil 33748 df-ltrn 33749

This theorem is referenced by: trlcnv 33809 trlcocnv 34364 trlcoabs2N 34366 trlcoat 34367 trlcocnvat 34368 trlcone 34372 cdlemg46 34379 tgrpgrplem 34393 tendoicl 34440 cdlemh1 34459 cdlemh2 34460 cdlemh 34461 cdlemi2 34463 cdlemi 34464 cdlemk2 34476 cdlemk3 34477 cdlemk4 34478 cdlemk8 34482 cdlemk9 34483 cdlemk9bN 34484 cdlemkvcl 34486 cdlemk10 34487 cdlemk11 34493 cdlemk12 34494 cdlemk14 34498 cdlemk11u 34515 cdlemk12u 34516 cdlemk37 34558 cdlemkfid1N 34565 cdlemkid1 34566 cdlemkid2 34568 tendocnv 34666 tendospcanN 34668 dvhgrp 34752 cdlemn8 34849 dihopelvalcpre 34893 dih1 34931 dihglbcpreN 34945 dihjatcclem3 35065 dihjatcclem4 35066

W3C validator