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.
StepHypRef Expression
1 ltrncnv.h . . . 4
2 eqid 2471 . . . 4
3 ltrncnv.t . . . 4
41, 2, 3ltrnldil 33758 . . 3
51, 2ldilcnv 33751 . . 3
64, 5syldan 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
1412, 13, 1, 3ltrncnvel 33778 . . . . . . 7
158, 9, 10, 11, 14syl112anc 1296 . . . . . 6
16 simp2r 1057 . . . . . . 7
17 simp3r 1059 . . . . . . 7
1812, 13, 1, 3ltrncnvel 33778 . . . . . . 7
198, 9, 16, 17, 18syl112anc 1296 . . . . . 6
20 eqid 2471 . . . . . . 7
21 eqid 2471 . . . . . . 7
2212, 20, 21, 13, 1, 3ltrnu 33757 . . . . . 6
237, 15, 19, 22syl3anc 1292 . . . . 5
24 eqid 2471 . . . . . . . . . . 11
2524, 1, 3ltrn1o 33760 . . . . . . . . . 10
26253ad2ant1 1051 . . . . . . . . 9
2724, 13atbase 32926 . . . . . . . . . 10
2810, 27syl 17 . . . . . . . . 9
29 f1ocnvfv2 6194 . . . . . . . . 9
3026, 28, 29syl2anc 673 . . . . . . . 8
3130oveq2d 6324 . . . . . . 7
32 simp1ll 1093 . . . . . . . 8
3312, 13, 1, 3ltrncnvat 33777 . . . . . . . . 9
348, 9, 10, 33syl3anc 1292 . . . . . . . 8
3520, 13hlatjcom 33004 . . . . . . . 8
3632, 34, 10, 35syl3anc 1292 . . . . . . 7
3731, 36eqtrd 2505 . . . . . 6
3837oveq1d 6323 . . . . 5
3924, 13atbase 32926 . . . . . . . . . 10
4016, 39syl 17 . . . . . . . . 9
41 f1ocnvfv2 6194 . . . . . . . . 9
4226, 40, 41syl2anc 673 . . . . . . . 8
4342oveq2d 6324 . . . . . . 7
4412, 13, 1, 3ltrncnvat 33777 . . . . . . . . 9
458, 9, 16, 44syl3anc 1292 . . . . . . . 8
4620, 13hlatjcom 33004 . . . . . . . 8
4732, 45, 16, 46syl3anc 1292 . . . . . . 7
4843, 47eqtrd 2505 . . . . . 6
4948oveq1d 6323 . . . . 5
5023, 38, 493eqtr3d 2513 . . . 4
51503exp 1230 . . 3
5251ralrimivv 2813 . 2
5312, 20, 21, 13, 1, 2, 3isltrn 33755 . . 3