Metamath Proof Explorer


Theorem lautset

Description: The set of lattice automorphisms. (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lautset.b B = Base K
lautset.l ˙ = K
lautset.i I = LAut K
Assertion lautset K A I = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y

Proof

Step Hyp Ref Expression
1 lautset.b B = Base K
2 lautset.l ˙ = K
3 lautset.i I = LAut K
4 elex K A K V
5 fveq2 k = K Base k = Base K
6 5 1 eqtr4di k = K Base k = B
7 6 f1oeq2d k = K f : Base k 1-1 onto Base k f : B 1-1 onto Base k
8 f1oeq3 Base k = B f : B 1-1 onto Base k f : B 1-1 onto B
9 6 8 syl k = K f : B 1-1 onto Base k f : B 1-1 onto B
10 7 9 bitrd k = K f : Base k 1-1 onto Base k f : B 1-1 onto B
11 fveq2 k = K k = K
12 11 2 eqtr4di k = K k = ˙
13 12 breqd k = K x k y x ˙ y
14 12 breqd k = K f x k f y f x ˙ f y
15 13 14 bibi12d k = K x k y f x k f y x ˙ y f x ˙ f y
16 6 15 raleqbidv k = K y Base k x k y f x k f y y B x ˙ y f x ˙ f y
17 6 16 raleqbidv k = K x Base k y Base k x k y f x k f y x B y B x ˙ y f x ˙ f y
18 10 17 anbi12d k = K f : Base k 1-1 onto Base k x Base k y Base k x k y f x k f y f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
19 18 abbidv k = K f | f : Base k 1-1 onto Base k x Base k y Base k x k y f x k f y = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
20 df-laut LAut = k V f | f : Base k 1-1 onto Base k x Base k y Base k x k y f x k f y
21 1 fvexi B V
22 21 21 mapval B B = f | f : B B
23 ovex B B V
24 22 23 eqeltrri f | f : B B V
25 f1of f : B 1-1 onto B f : B B
26 25 ss2abi f | f : B 1-1 onto B f | f : B B
27 24 26 ssexi f | f : B 1-1 onto B V
28 simpl f : B 1-1 onto B x B y B x ˙ y f x ˙ f y f : B 1-1 onto B
29 28 ss2abi f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y f | f : B 1-1 onto B
30 27 29 ssexi f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y V
31 19 20 30 fvmpt K V LAut K = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
32 3 31 syl5eq K V I = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
33 4 32 syl K A I = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y