Metamath Proof Explorer


Theorem islaut

Description: The predictate "is a lattice automorphism." (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lautset.b B = Base K
lautset.l ˙ = K
lautset.i I = LAut K
Assertion islaut K A F I 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 1 2 3 lautset K A I = f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
5 4 eleq2d K A F I F f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y
6 f1of F : B 1-1 onto B F : B B
7 1 fvexi B V
8 fex F : B B B V F V
9 6 7 8 sylancl F : B 1-1 onto B F V
10 9 adantr F : B 1-1 onto B x B y B x ˙ y F x ˙ F y F V
11 f1oeq1 f = F f : B 1-1 onto B F : B 1-1 onto B
12 fveq1 f = F f x = F x
13 fveq1 f = F f y = F y
14 12 13 breq12d f = F f x ˙ f y F x ˙ F y
15 14 bibi2d f = F x ˙ y f x ˙ f y x ˙ y F x ˙ F y
16 15 2ralbidv f = F x B y B x ˙ y f x ˙ f y x B y B x ˙ y F x ˙ F y
17 11 16 anbi12d f = F f : B 1-1 onto B x B y B x ˙ y f x ˙ f y F : B 1-1 onto B x B y B x ˙ y F x ˙ F y
18 10 17 elab3 F f | f : B 1-1 onto B x B y B x ˙ y f x ˙ f y F : B 1-1 onto B x B y B x ˙ y F x ˙ F y
19 5 18 bitrdi K A F I F : B 1-1 onto B x B y B x ˙ y F x ˙ F y