Metamath Proof Explorer

Theorem lauteq

Description: A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses lauteq.b 
|- B = ( Base ` K )
lauteq.a 
|- A = ( Atoms ` K )
lauteq.i 
|- I = ( LAut ` K )
Assertion lauteq 
|- ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> ( F ` X ) = X )

Proof

Step Hyp Ref Expression
1 lauteq.b 
 |-  B = ( Base ` K )
2 lauteq.a 
 |-  A = ( Atoms ` K )
3 lauteq.i 
 |-  I = ( LAut ` K )
4 simpl1 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> K e. HL )
5 simpl2 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> F e. I )
6 1 2 atbase 
 |-  ( p e. A -> p e. B )
7 6 adantl 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> p e. B )
8 simpl3 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> X e. B )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 1 9 3 lautle 
 |-  ( ( ( K e. HL /\ F e. I ) /\ ( p e. B /\ X e. B ) ) -> ( p ( le ` K ) X <-> ( F ` p ) ( le ` K ) ( F ` X ) ) )
11 4 5 7 8 10 syl22anc 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> ( p ( le ` K ) X <-> ( F ` p ) ( le ` K ) ( F ` X ) ) )
12 breq1 
 |-  ( ( F ` p ) = p -> ( ( F ` p ) ( le ` K ) ( F ` X ) <-> p ( le ` K ) ( F ` X ) ) )
13 11 12 sylan9bb 
 |-  ( ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) /\ ( F ` p ) = p ) -> ( p ( le ` K ) X <-> p ( le ` K ) ( F ` X ) ) )
14 13 bicomd 
 |-  ( ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) /\ ( F ` p ) = p ) -> ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) )
15 14 ex 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ p e. A ) -> ( ( F ` p ) = p -> ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) ) )
16 15 ralimdva 
 |-  ( ( K e. HL /\ F e. I /\ X e. B ) -> ( A. p e. A ( F ` p ) = p -> A. p e. A ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) ) )
17 16 imp 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> A. p e. A ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) )
18 simpl1 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> K e. HL )
19 simpl2 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> F e. I )
20 simpl3 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> X e. B )
21 1 3 lautcl 
 |-  ( ( ( K e. HL /\ F e. I ) /\ X e. B ) -> ( F ` X ) e. B )
22 18 19 20 21 syl21anc 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> ( F ` X ) e. B )
23 1 9 2 hlateq 
 |-  ( ( K e. HL /\ ( F ` X ) e. B /\ X e. B ) -> ( A. p e. A ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) <-> ( F ` X ) = X ) )
24 18 22 20 23 syl3anc 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> ( A. p e. A ( p ( le ` K ) ( F ` X ) <-> p ( le ` K ) X ) <-> ( F ` X ) = X ) )
25 17 24 mpbid 
 |-  ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> ( F ` X ) = X )