Metamath Proof Explorer

Theorem trlord

Description: The ordering of two Hilbert lattice elements (under the fiducial hyperplane W ) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014)

Ref Expression
Hypotheses trlord.b 
|- B = ( Base ` K )
trlord.l 
|- .<_ = ( le ` K )
trlord.a 
|- A = ( Atoms ` K )
trlord.h 
|- H = ( LHyp ` K )
trlord.t 
|- T = ( ( LTrn ` K ) ` W )
trlord.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlord 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y <-> A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) ) )

Proof

Step Hyp Ref Expression
1 trlord.b 
 |-  B = ( Base ` K )
2 trlord.l 
 |-  .<_ = ( le ` K )
3 trlord.a 
 |-  A = ( Atoms ` K )
4 trlord.h 
 |-  H = ( LHyp ` K )
5 trlord.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 trlord.r 
 |-  R = ( ( trL ` K ) ` W )
7 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> K e. Lat )
9 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> ( K e. HL /\ W e. H ) )
10 simprlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> f e. T )
11 1 4 5 6 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) e. B )
12 9 10 11 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> ( R ` f ) e. B )
13 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> X e. B )
14 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> Y e. B )
15 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> ( R ` f ) .<_ X )
16 simprll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> X .<_ Y )
17 1 2 8 12 13 14 15 16 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( ( X .<_ Y /\ f e. T ) /\ ( R ` f ) .<_ X ) ) -> ( R ` f ) .<_ Y )
18 17 exp44 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y -> ( f e. T -> ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) ) ) )
19 18 ralrimdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y -> A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) ) )
20 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> K e. HL )
21 20 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> K e. Lat )
22 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> u e. A )
23 1 3 atbase 
 |-  ( u e. A -> u e. B )
24 22 23 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> u e. B )
25 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> X e. B )
26 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> W e. H )
27 1 4 lhpbase 
 |-  ( W e. H -> W e. B )
28 26 27 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> W e. B )
29 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> u .<_ X )
30 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> X .<_ W )
31 1 2 21 24 25 28 29 30 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> u .<_ W )
32 31 29 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ X ) -> ( u .<_ W /\ u .<_ X ) )
33 32 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) ) -> ( u .<_ X -> ( u .<_ W /\ u .<_ X ) ) )
34 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> ( K e. HL /\ W e. H ) )
35 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> u e. A )
36 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> u .<_ W )
37 2 3 4 5 6 cdlemf 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. A /\ u .<_ W ) ) -> E. g e. T ( R ` g ) = u )
38 34 35 36 37 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> E. g e. T ( R ` g ) = u )
39 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) )
40 fveq2 
 |-  ( f = g -> ( R ` f ) = ( R ` g ) )
41 40 breq1d 
 |-  ( f = g -> ( ( R ` f ) .<_ X <-> ( R ` g ) .<_ X ) )
42 40 breq1d 
 |-  ( f = g -> ( ( R ` f ) .<_ Y <-> ( R ` g ) .<_ Y ) )
43 41 42 imbi12d 
 |-  ( f = g -> ( ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) <-> ( ( R ` g ) .<_ X -> ( R ` g ) .<_ Y ) ) )
44 43 rspccv 
 |-  ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) -> ( g e. T -> ( ( R ` g ) .<_ X -> ( R ` g ) .<_ Y ) ) )
45 39 44 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> ( g e. T -> ( ( R ` g ) .<_ X -> ( R ` g ) .<_ Y ) ) )
46 breq1 
 |-  ( ( R ` g ) = u -> ( ( R ` g ) .<_ X <-> u .<_ X ) )
47 breq1 
 |-  ( ( R ` g ) = u -> ( ( R ` g ) .<_ Y <-> u .<_ Y ) )
48 46 47 imbi12d 
 |-  ( ( R ` g ) = u -> ( ( ( R ` g ) .<_ X -> ( R ` g ) .<_ Y ) <-> ( u .<_ X -> u .<_ Y ) ) )
49 48 biimpcd 
 |-  ( ( ( R ` g ) .<_ X -> ( R ` g ) .<_ Y ) -> ( ( R ` g ) = u -> ( u .<_ X -> u .<_ Y ) ) )
50 45 49 syl6 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> ( g e. T -> ( ( R ` g ) = u -> ( u .<_ X -> u .<_ Y ) ) ) )
51 50 rexlimdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> ( E. g e. T ( R ` g ) = u -> ( u .<_ X -> u .<_ Y ) ) )
52 38 51 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) /\ u .<_ W ) -> ( u .<_ X -> u .<_ Y ) )
53 52 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) ) -> ( u .<_ W -> ( u .<_ X -> u .<_ Y ) ) )
54 53 impd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) ) -> ( ( u .<_ W /\ u .<_ X ) -> u .<_ Y ) )
55 33 54 syld 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) /\ u e. A ) ) -> ( u .<_ X -> u .<_ Y ) )
56 55 exp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) -> ( u e. A -> ( u .<_ X -> u .<_ Y ) ) ) )
57 56 ralrimdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) -> A. u e. A ( u .<_ X -> u .<_ Y ) ) )
58 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> K e. HL )
59 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> X e. B )
60 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> Y e. B )
61 1 2 3 hlatle 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. u e. A ( u .<_ X -> u .<_ Y ) ) )
62 58 59 60 61 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y <-> A. u e. A ( u .<_ X -> u .<_ Y ) ) )
63 57 62 sylibrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) -> X .<_ Y ) )
64 19 63 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X .<_ Y <-> A. f e. T ( ( R ` f ) .<_ X -> ( R ` f ) .<_ Y ) ) )