Metamath Proof Explorer

Theorem cdlemk4

Description: Part of proof of Lemma K of Crawley p. 118, last line. We use X for their h, since H is already used. (Contributed by NM, 24-Jun-2013)

Ref Expression
Hypotheses cdlemk.b 
|- B = ( Base ` K )
cdlemk.l 
|- .<_ = ( le ` K )
cdlemk.j 
|- .\/ = ( join ` K )
cdlemk.a 
|- A = ( Atoms ` K )
cdlemk.h 
|- H = ( LHyp ` K )
cdlemk.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemk.r 
|- R = ( ( trL ` K ) ` W )
cdlemk.m 
|- ./\ = ( meet ` K )
Assertion cdlemk4 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) .<_ ( ( X ` P ) .\/ ( R ` ( X o. `' F ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk.b 
 |-  B = ( Base ` K )
2 cdlemk.l 
 |-  .<_ = ( le ` K )
3 cdlemk.j 
 |-  .\/ = ( join ` K )
4 cdlemk.a 
 |-  A = ( Atoms ` K )
5 cdlemk.h 
 |-  H = ( LHyp ` K )
6 cdlemk.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemk.r 
 |-  R = ( ( trL ` K ) ` W )
8 cdlemk.m 
 |-  ./\ = ( meet ` K )
9 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL )
10 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
11 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F e. T )
12 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A )
13 2 4 5 6 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( F ` P ) e. A )
14 10 11 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) e. A )
15 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> X e. T )
16 2 4 5 6 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ P e. A ) -> ( X ` P ) e. A )
17 10 15 12 16 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X ` P ) e. A )
18 2 3 4 hlatlej1 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ ( X ` P ) e. A ) -> ( F ` P ) .<_ ( ( F ` P ) .\/ ( X ` P ) ) )
19 9 14 17 18 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) .<_ ( ( F ` P ) .\/ ( X ` P ) ) )
20 9 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. Lat )
21 1 4 atbase 
 |-  ( ( F ` P ) e. A -> ( F ` P ) e. B )
22 14 21 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) e. B )
23 1 4 atbase 
 |-  ( ( X ` P ) e. A -> ( X ` P ) e. B )
24 17 23 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X ` P ) e. B )
25 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( F ` P ) e. B /\ ( X ` P ) e. B ) -> ( ( F ` P ) .\/ ( X ` P ) ) e. B )
26 20 22 24 25 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( X ` P ) ) e. B )
27 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. H )
28 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
29 27 28 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. B )
30 2 3 4 hlatlej2 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ ( X ` P ) e. A ) -> ( X ` P ) .<_ ( ( F ` P ) .\/ ( X ` P ) ) )
31 9 14 17 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X ` P ) .<_ ( ( F ` P ) .\/ ( X ` P ) ) )
32 1 2 3 8 4 atmod3i1 
 |-  ( ( K e. HL /\ ( ( X ` P ) e. A /\ ( ( F ` P ) .\/ ( X ` P ) ) e. B /\ W e. B ) /\ ( X ` P ) .<_ ( ( F ` P ) .\/ ( X ` P ) ) ) -> ( ( X ` P ) .\/ ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ W ) ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( ( X ` P ) .\/ W ) ) )
33 9 17 26 29 31 32 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( X ` P ) .\/ ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ W ) ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( ( X ` P ) .\/ W ) ) )
34 5 6 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
35 10 11 34 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> `' F e. T )
36 5 6 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ `' F e. T ) -> ( X o. `' F ) e. T )
37 10 15 35 36 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X o. `' F ) e. T )
38 2 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 ) )
39 11 38 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
40 2 3 8 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X o. `' F ) e. T /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) -> ( R ` ( X o. `' F ) ) = ( ( ( F ` P ) .\/ ( ( X o. `' F ) ` ( F ` P ) ) ) ./\ W ) )
41 10 37 39 40 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( X o. `' F ) ) = ( ( ( F ` P ) .\/ ( ( X o. `' F ) ` ( F ` P ) ) ) ./\ W ) )
42 1 5 6 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B )
43 10 11 42 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F : B -1-1-onto-> B )
44 f1ococnv1 
 |-  ( F : B -1-1-onto-> B -> ( `' F o. F ) = ( _I |` B ) )
45 43 44 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( `' F o. F ) = ( _I |` B ) )
46 45 coeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X o. ( `' F o. F ) ) = ( X o. ( _I |` B ) ) )
47 1 5 6 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T ) -> X : B -1-1-onto-> B )
48 10 15 47 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> X : B -1-1-onto-> B )
49 f1of 
 |-  ( X : B -1-1-onto-> B -> X : B --> B )
50 fcoi1 
 |-  ( X : B --> B -> ( X o. ( _I |` B ) ) = X )
51 48 49 50 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X o. ( _I |` B ) ) = X )
52 46 51 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> X = ( X o. ( `' F o. F ) ) )
53 coass 
 |-  ( ( X o. `' F ) o. F ) = ( X o. ( `' F o. F ) )
54 52 53 eqtr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> X = ( ( X o. `' F ) o. F ) )
55 54 fveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X ` P ) = ( ( ( X o. `' F ) o. F ) ` P ) )
56 2 4 5 6 ltrncoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X o. `' F ) e. T /\ F e. T ) /\ P e. A ) -> ( ( ( X o. `' F ) o. F ) ` P ) = ( ( X o. `' F ) ` ( F ` P ) ) )
57 10 37 11 12 56 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( X o. `' F ) o. F ) ` P ) = ( ( X o. `' F ) ` ( F ` P ) ) )
58 55 57 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X ` P ) = ( ( X o. `' F ) ` ( F ` P ) ) )
59 58 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( X ` P ) ) = ( ( F ` P ) .\/ ( ( X o. `' F ) ` ( F ` P ) ) ) )
60 59 eqcomd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( ( X o. `' F ) ` ( F ` P ) ) ) = ( ( F ` P ) .\/ ( X ` P ) ) )
61 60 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( ( X o. `' F ) ` ( F ` P ) ) ) ./\ W ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ W ) )
62 41 61 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( X o. `' F ) ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ W ) )
63 62 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( X ` P ) .\/ ( R ` ( X o. `' F ) ) ) = ( ( X ` P ) .\/ ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ W ) ) )
64 2 4 5 6 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( X ` P ) e. A /\ -. ( X ` P ) .<_ W ) )
65 15 64 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( X ` P ) e. A /\ -. ( X ` P ) .<_ W ) )
66 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
67 2 3 66 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ` P ) e. A /\ -. ( X ` P ) .<_ W ) ) -> ( ( X ` P ) .\/ W ) = ( 1. ` K ) )
68 10 65 67 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( X ` P ) .\/ W ) = ( 1. ` K ) )
69 68 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( ( X ` P ) .\/ W ) ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( 1. ` K ) ) )
70 hlol 
 |-  ( K e. HL -> K e. OL )
71 9 70 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. OL )
72 1 8 66 olm11 
 |-  ( ( K e. OL /\ ( ( F ` P ) .\/ ( X ` P ) ) e. B ) -> ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( 1. ` K ) ) = ( ( F ` P ) .\/ ( X ` P ) ) )
73 71 26 72 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( 1. ` K ) ) = ( ( F ` P ) .\/ ( X ` P ) ) )
74 69 73 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( X ` P ) ) = ( ( ( F ` P ) .\/ ( X ` P ) ) ./\ ( ( X ` P ) .\/ W ) ) )
75 33 63 74 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( X ` P ) ) = ( ( X ` P ) .\/ ( R ` ( X o. `' F ) ) ) )
76 19 75 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) .<_ ( ( X ` P ) .\/ ( R ` ( X o. `' F ) ) ) )