Metamath Proof Explorer

Theorem dia2dimlem2

Description: Lemma for dia2dim . Define a translation G whose trace is atom U . Part of proof of Lemma M in Crawley p. 121 line 4. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem2.l 
|- .<_ = ( le ` K )
dia2dimlem2.j 
|- .\/ = ( join ` K )
dia2dimlem2.m 
|- ./\ = ( meet ` K )
dia2dimlem2.a 
|- A = ( Atoms ` K )
dia2dimlem2.h 
|- H = ( LHyp ` K )
dia2dimlem2.t 
|- T = ( ( LTrn ` K ) ` W )
dia2dimlem2.r 
|- R = ( ( trL ` K ) ` W )
dia2dimlem2.q 
|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
dia2dimlem2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dia2dimlem2.u 
|- ( ph -> ( U e. A /\ U .<_ W ) )
dia2dimlem2.v 
|- ( ph -> ( V e. A /\ V .<_ W ) )
dia2dimlem2.p 
|- ( ph -> ( P e. A /\ -. P .<_ W ) )
dia2dimlem2.f 
|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
dia2dimlem2.rf 
|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
dia2dimlem2.rv 
|- ( ph -> ( R ` F ) =/= V )
dia2dimlem2.g 
|- ( ph -> G e. T )
dia2dimlem2.gv 
|- ( ph -> ( G ` P ) = Q )
Assertion dia2dimlem2 
|- ( ph -> ( R ` G ) = U )

Proof

Step Hyp Ref Expression
1 dia2dimlem2.l 
 |-  .<_ = ( le ` K )
2 dia2dimlem2.j 
 |-  .\/ = ( join ` K )
3 dia2dimlem2.m 
 |-  ./\ = ( meet ` K )
4 dia2dimlem2.a 
 |-  A = ( Atoms ` K )
5 dia2dimlem2.h 
 |-  H = ( LHyp ` K )
6 dia2dimlem2.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 dia2dimlem2.r 
 |-  R = ( ( trL ` K ) ` W )
8 dia2dimlem2.q 
 |-  Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
9 dia2dimlem2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 dia2dimlem2.u 
 |-  ( ph -> ( U e. A /\ U .<_ W ) )
11 dia2dimlem2.v 
 |-  ( ph -> ( V e. A /\ V .<_ W ) )
12 dia2dimlem2.p 
 |-  ( ph -> ( P e. A /\ -. P .<_ W ) )
13 dia2dimlem2.f 
 |-  ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
14 dia2dimlem2.rf 
 |-  ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
15 dia2dimlem2.rv 
 |-  ( ph -> ( R ` F ) =/= V )
16 dia2dimlem2.g 
 |-  ( ph -> G e. T )
17 dia2dimlem2.gv 
 |-  ( ph -> ( G ` P ) = Q )
18 9 simpld 
 |-  ( ph -> K e. HL )
19 18 hllatd 
 |-  ( ph -> K e. Lat )
20 12 simpld 
 |-  ( ph -> P e. A )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 21 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
23 20 22 syl 
 |-  ( ph -> P e. ( Base ` K ) )
24 10 simpld 
 |-  ( ph -> U e. A )
25 21 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ph -> U e. ( Base ` K ) )
27 21 1 2 latlej2 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> U .<_ ( P .\/ U ) )
28 19 23 26 27 syl3anc 
 |-  ( ph -> U .<_ ( P .\/ U ) )
29 21 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ U e. A ) -> ( P .\/ U ) e. ( Base ` K ) )
30 18 20 24 29 syl3anc 
 |-  ( ph -> ( P .\/ U ) e. ( Base ` K ) )
31 21 1 3 latleeqm2 
 |-  ( ( K e. Lat /\ U e. ( Base ` K ) /\ ( P .\/ U ) e. ( Base ` K ) ) -> ( U .<_ ( P .\/ U ) <-> ( ( P .\/ U ) ./\ U ) = U ) )
32 19 26 30 31 syl3anc 
 |-  ( ph -> ( U .<_ ( P .\/ U ) <-> ( ( P .\/ U ) ./\ U ) = U ) )
33 28 32 mpbid 
 |-  ( ph -> ( ( P .\/ U ) ./\ U ) = U )
34 1 4 5 6 7 trlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F e. T /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
35 9 12 13 34 syl3anc 
 |-  ( ph -> ( R ` F ) e. A )
36 11 simpld 
 |-  ( ph -> V e. A )
37 1 2 4 hlatexch2 
 |-  ( ( K e. HL /\ ( ( R ` F ) e. A /\ U e. A /\ V e. A ) /\ ( R ` F ) =/= V ) -> ( ( R ` F ) .<_ ( U .\/ V ) -> U .<_ ( ( R ` F ) .\/ V ) ) )
38 18 35 24 36 15 37 syl131anc 
 |-  ( ph -> ( ( R ` F ) .<_ ( U .\/ V ) -> U .<_ ( ( R ` F ) .\/ V ) ) )
39 14 38 mpd 
 |-  ( ph -> U .<_ ( ( R ` F ) .\/ V ) )
40 13 simpld 
 |-  ( ph -> F e. T )
41 1 2 3 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
42 9 40 12 41 syl3anc 
 |-  ( ph -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
43 42 oveq1d 
 |-  ( ph -> ( ( R ` F ) .\/ V ) = ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ V ) )
44 1 4 5 6 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
45 9 40 12 44 syl3anc 
 |-  ( ph -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
46 45 simpld 
 |-  ( ph -> ( F ` P ) e. A )
47 21 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
48 18 20 46 47 syl3anc 
 |-  ( ph -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
49 9 simprd 
 |-  ( ph -> W e. H )
50 21 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
51 49 50 syl 
 |-  ( ph -> W e. ( Base ` K ) )
52 11 simprd 
 |-  ( ph -> V .<_ W )
53 21 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( V e. A /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ V .<_ W ) -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ V ) = ( ( ( P .\/ ( F ` P ) ) .\/ V ) ./\ W ) )
54 18 36 48 51 52 53 syl131anc 
 |-  ( ph -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ V ) = ( ( ( P .\/ ( F ` P ) ) .\/ V ) ./\ W ) )
55 2 4 hlatjass 
 |-  ( ( K e. HL /\ ( P e. A /\ ( F ` P ) e. A /\ V e. A ) ) -> ( ( P .\/ ( F ` P ) ) .\/ V ) = ( P .\/ ( ( F ` P ) .\/ V ) ) )
56 18 20 46 36 55 syl13anc 
 |-  ( ph -> ( ( P .\/ ( F ` P ) ) .\/ V ) = ( P .\/ ( ( F ` P ) .\/ V ) ) )
57 56 oveq1d 
 |-  ( ph -> ( ( ( P .\/ ( F ` P ) ) .\/ V ) ./\ W ) = ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) )
58 54 57 eqtrd 
 |-  ( ph -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ V ) = ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) )
59 43 58 eqtrd 
 |-  ( ph -> ( ( R ` F ) .\/ V ) = ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) )
60 39 59 breqtrd 
 |-  ( ph -> U .<_ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) )
61 21 2 4 hlatjcl 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
62 18 46 36 61 syl3anc 
 |-  ( ph -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
63 21 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) ) -> ( P .\/ ( ( F ` P ) .\/ V ) ) e. ( Base ` K ) )
64 19 23 62 63 syl3anc 
 |-  ( ph -> ( P .\/ ( ( F ` P ) .\/ V ) ) e. ( Base ` K ) )
65 21 3 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ ( ( F ` P ) .\/ V ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) e. ( Base ` K ) )
66 19 64 51 65 syl3anc 
 |-  ( ph -> ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) e. ( Base ` K ) )
67 21 1 3 latmlem2 
 |-  ( ( K e. Lat /\ ( U e. ( Base ` K ) /\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) e. ( Base ` K ) /\ ( P .\/ U ) e. ( Base ` K ) ) ) -> ( U .<_ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) -> ( ( P .\/ U ) ./\ U ) .<_ ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) ) )
68 19 26 66 30 67 syl13anc 
 |-  ( ph -> ( U .<_ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) -> ( ( P .\/ U ) ./\ U ) .<_ ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) ) )
69 60 68 mpd 
 |-  ( ph -> ( ( P .\/ U ) ./\ U ) .<_ ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
70 33 69 eqbrtrrd 
 |-  ( ph -> U .<_ ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
71 1 2 3 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
72 9 16 12 71 syl3anc 
 |-  ( ph -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
73 17 8 eqtrdi 
 |-  ( ph -> ( G ` P ) = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
74 73 oveq2d 
 |-  ( ph -> ( P .\/ ( G ` P ) ) = ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) )
75 74 oveq1d 
 |-  ( ph -> ( ( P .\/ ( G ` P ) ) ./\ W ) = ( ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) ./\ W ) )
76 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ U e. A ) -> P .<_ ( P .\/ U ) )
77 18 20 24 76 syl3anc 
 |-  ( ph -> P .<_ ( P .\/ U ) )
78 21 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( P .\/ U ) e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) ) /\ P .<_ ( P .\/ U ) ) -> ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) = ( ( P .\/ U ) ./\ ( P .\/ ( ( F ` P ) .\/ V ) ) ) )
79 18 20 30 62 77 78 syl131anc 
 |-  ( ph -> ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) = ( ( P .\/ U ) ./\ ( P .\/ ( ( F ` P ) .\/ V ) ) ) )
80 79 oveq1d 
 |-  ( ph -> ( ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) ./\ W ) = ( ( ( P .\/ U ) ./\ ( P .\/ ( ( F ` P ) .\/ V ) ) ) ./\ W ) )
81 hlol 
 |-  ( K e. HL -> K e. OL )
82 18 81 syl 
 |-  ( ph -> K e. OL )
83 21 3 latmassOLD 
 |-  ( ( K e. OL /\ ( ( P .\/ U ) e. ( Base ` K ) /\ ( P .\/ ( ( F ` P ) .\/ V ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( P .\/ U ) ./\ ( P .\/ ( ( F ` P ) .\/ V ) ) ) ./\ W ) = ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
84 82 30 64 51 83 syl13anc 
 |-  ( ph -> ( ( ( P .\/ U ) ./\ ( P .\/ ( ( F ` P ) .\/ V ) ) ) ./\ W ) = ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
85 80 84 eqtrd 
 |-  ( ph -> ( ( P .\/ ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) ./\ W ) = ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
86 75 85 eqtrd 
 |-  ( ph -> ( ( P .\/ ( G ` P ) ) ./\ W ) = ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
87 72 86 eqtrd 
 |-  ( ph -> ( R ` G ) = ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) )
88 87 eqcomd 
 |-  ( ph -> ( ( P .\/ U ) ./\ ( ( P .\/ ( ( F ` P ) .\/ V ) ) ./\ W ) ) = ( R ` G ) )
89 70 88 breqtrd 
 |-  ( ph -> U .<_ ( R ` G ) )
90 hlatl 
 |-  ( K e. HL -> K e. AtLat )
91 18 90 syl 
 |-  ( ph -> K e. AtLat )
92 hlop 
 |-  ( K e. HL -> K e. OP )
93 18 92 syl 
 |-  ( ph -> K e. OP )
94 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
95 eqid 
 |-  ( lt ` K ) = ( lt ` K )
96 94 95 4 0ltat 
 |-  ( ( K e. OP /\ U e. A ) -> ( 0. ` K ) ( lt ` K ) U )
97 93 24 96 syl2anc 
 |-  ( ph -> ( 0. ` K ) ( lt ` K ) U )
98 hlpos 
 |-  ( K e. HL -> K e. Poset )
99 18 98 syl 
 |-  ( ph -> K e. Poset )
100 21 94 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
101 93 100 syl 
 |-  ( ph -> ( 0. ` K ) e. ( Base ` K ) )
102 21 5 6 7 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) e. ( Base ` K ) )
103 9 16 102 syl2anc 
 |-  ( ph -> ( R ` G ) e. ( Base ` K ) )
104 21 1 95 pltletr 
 |-  ( ( K e. Poset /\ ( ( 0. ` K ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ ( R ` G ) e. ( Base ` K ) ) ) -> ( ( ( 0. ` K ) ( lt ` K ) U /\ U .<_ ( R ` G ) ) -> ( 0. ` K ) ( lt ` K ) ( R ` G ) ) )
105 99 101 26 103 104 syl13anc 
 |-  ( ph -> ( ( ( 0. ` K ) ( lt ` K ) U /\ U .<_ ( R ` G ) ) -> ( 0. ` K ) ( lt ` K ) ( R ` G ) ) )
106 97 89 105 mp2and 
 |-  ( ph -> ( 0. ` K ) ( lt ` K ) ( R ` G ) )
107 21 95 94 opltn0 
 |-  ( ( K e. OP /\ ( R ` G ) e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) ( R ` G ) <-> ( R ` G ) =/= ( 0. ` K ) ) )
108 93 103 107 syl2anc 
 |-  ( ph -> ( ( 0. ` K ) ( lt ` K ) ( R ` G ) <-> ( R ` G ) =/= ( 0. ` K ) ) )
109 106 108 mpbid 
 |-  ( ph -> ( R ` G ) =/= ( 0. ` K ) )
110 109 neneqd 
 |-  ( ph -> -. ( R ` G ) = ( 0. ` K ) )
111 94 4 5 6 7 trlator0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( ( R ` G ) e. A \/ ( R ` G ) = ( 0. ` K ) ) )
112 9 16 111 syl2anc 
 |-  ( ph -> ( ( R ` G ) e. A \/ ( R ` G ) = ( 0. ` K ) ) )
113 112 orcomd 
 |-  ( ph -> ( ( R ` G ) = ( 0. ` K ) \/ ( R ` G ) e. A ) )
114 113 ord 
 |-  ( ph -> ( -. ( R ` G ) = ( 0. ` K ) -> ( R ` G ) e. A ) )
115 110 114 mpd 
 |-  ( ph -> ( R ` G ) e. A )
116 1 4 atcmp 
 |-  ( ( K e. AtLat /\ U e. A /\ ( R ` G ) e. A ) -> ( U .<_ ( R ` G ) <-> U = ( R ` G ) ) )
117 91 24 115 116 syl3anc 
 |-  ( ph -> ( U .<_ ( R ` G ) <-> U = ( R ` G ) ) )
118 89 117 mpbid 
 |-  ( ph -> U = ( R ` G ) )
119 118 eqcomd 
 |-  ( ph -> ( R ` G ) = U )