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 36286

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 2454	. . . 4
3		ltrncnv.t	. . . 4
4	1, 2, 3	ltrnldil 36262	. . 3 $/\$ $/\$
5	1, 2	ldilcnv 36255	. . 3 $/\$ $/\$
6	4, 5	syldan 468	. 2 $/\$ $/\$
7		simp1 994	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simp1l 1018	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		simp1r 1019	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simp2l 1020	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simp3l 1022	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2454	. . . . . . . 8
13		eqid 2454	. . . . . . . 8
14	12, 13, 1, 3	ltrncnvel 36282	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	8, 9, 10, 11, 14	syl112anc 1230	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp2r 1021	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp3r 1023	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	12, 13, 1, 3	ltrncnvel 36282	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
19	8, 9, 16, 17, 18	syl112anc 1230	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqid 2454	. . . . . . 7
21		eqid 2454	. . . . . . 7
22	12, 20, 21, 13, 1, 3	ltrnu 36261	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23	7, 15, 19, 22	syl3anc 1226	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		eqid 2454	. . . . . . . . . . 11
25	24, 1, 3	ltrn1o 36264	. . . . . . . . . 10 $/\$ $/\$
26	25	3ad2ant1 1015	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	24, 13	atbase 35430	. . . . . . . . . 10
28	10, 27	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		f1ocnvfv2 6158	. . . . . . . . 9 $/\$
30	26, 28, 29	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	30	oveq2d 6286	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp1ll 1057	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	12, 13, 1, 3	ltrncnvat 36281	. . . . . . . . 9 $/\$ $/\$ $/\$
34	8, 9, 10, 33	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	20, 13	hlatjcom 35508	. . . . . . . 8 $/\$ $/\$
36	32, 34, 10, 35	syl3anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	31, 36	eqtrd 2495	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	oveq1d 6285	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	24, 13	atbase 35430	. . . . . . . . . 10
40	16, 39	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		f1ocnvfv2 6158	. . . . . . . . 9 $/\$
42	26, 40, 41	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	42	oveq2d 6286	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	12, 13, 1, 3	ltrncnvat 36281	. . . . . . . . 9 $/\$ $/\$ $/\$
45	8, 9, 16, 44	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	20, 13	hlatjcom 35508	. . . . . . . 8 $/\$ $/\$
47	32, 45, 16, 46	syl3anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	43, 47	eqtrd 2495	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	oveq1d 6285	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	23, 38, 49	3eqtr3d 2503	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	3exp 1193	. . 3 $/\$ $/\$ $/\$ $/\$
52	51	ralrimivv 2874	. 2 $/\$ $/\$ $/\$
53	12, 20, 21, 13, 1, 2, 3	isltrn 36259	. . 3 $/\$ $/\$ $/\$
54	53	adantr 463	. 2 $/\$ $/\$ $/\$ $/\$
55	6, 52, 54	mpbir2and 920	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wral 2804 class class class wbr 4439

ccnv 4987

wf1o 5569

cfv 5570 (class class class)co 6270

cbs 14719

cple 14794

cjn 15775

cmee 15776

catm 35404

chlt 35491

clh 36124

cldil 36240

cltrn 36241

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-id 4784 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-map 7414 df-preset 15759 df-poset 15777 df-plt 15790 df-lub 15806 df-glb 15807 df-join 15808 df-p0 15871 df-lat 15878 df-oposet 35317 df-ol 35319 df-oml 35320 df-covers 35407 df-ats 35408 df-atl 35439 df-cvlat 35463 df-hlat 35492 df-lhyp 36128 df-laut 36129 df-ldil 36244 df-ltrn 36245

This theorem is referenced by: trlcnv 36306 trlcocnv 36862 trlcoabs2N 36864 trlcoat 36865 trlcocnvat 36866 trlcone 36870 cdlemg46 36877 tgrpgrplem 36891 tendoicl 36938 cdlemh1 36957 cdlemh2 36958 cdlemh 36959 cdlemi2 36961 cdlemi 36962 cdlemk2 36974 cdlemk3 36975 cdlemk4 36976 cdlemk8 36980 cdlemk9 36981 cdlemk9bN 36982 cdlemkvcl 36984 cdlemk10 36985 cdlemk11 36991 cdlemk12 36992 cdlemk14 36996 cdlemk11u 37013 cdlemk12u 37014 cdlemk37 37056 cdlemkfid1N 37063 cdlemkid1 37064 cdlemkid2 37066 tendocnv 37164 tendospcanN 37166 dvhgrp 37250 cdlemn8 37347 dihopelvalcpre 37391 dih1 37429 dihglbcpreN 37443 dihjatcclem3 37563 dihjatcclem4 37564

W3C validator