This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dia2dimlem3

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

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

Proof

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