Metamath Proof Explorer


Theorem cdlemk9

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 29-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 cdlemk9
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ W ) = ( R ` ( X o. `' G ) ) )

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 1 2 3 4 5 6 7 8 cdlemk8
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) .\/ ( X ` P ) ) = ( ( G ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
10 9 oveq1d
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ W ) = ( ( ( G ` P ) .\/ ( R ` ( X o. `' G ) ) ) ./\ W ) )
11 simp1
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
12 2 4 5 6 ltrnel
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
13 12 3adant2r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
14 eqid
 |-  ( 0. ` K ) = ( 0. ` K )
15 2 8 14 4 5 lhpmat
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) -> ( ( G ` P ) ./\ W ) = ( 0. ` K ) )
16 11 13 15 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) ./\ W ) = ( 0. ` K ) )
17 16 oveq1d
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) ./\ W ) .\/ ( R ` ( X o. `' G ) ) ) = ( ( 0. ` K ) .\/ ( R ` ( X o. `' G ) ) ) )
18 simp1l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL )
19 simp2l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> G e. T )
20 simp3l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A )
21 2 4 5 6 ltrnat
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
22 11 19 20 21 syl3anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G ` P ) e. A )
23 simp2r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> X e. T )
24 5 6 ltrncnv
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
25 11 19 24 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> `' G e. T )
26 5 6 ltrnco
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ `' G e. T ) -> ( X o. `' G ) e. T )
27 11 23 25 26 syl3anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( X o. `' G ) e. T )
28 1 5 6 7 trlcl
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X o. `' G ) e. T ) -> ( R ` ( X o. `' G ) ) e. B )
29 11 27 28 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( X o. `' G ) ) e. B )
30 simp1r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. H )
31 1 5 lhpbase
 |-  ( W e. H -> W e. B )
32 30 31 syl
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. B )
33 2 5 6 7 trlle
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X o. `' G ) e. T ) -> ( R ` ( X o. `' G ) ) .<_ W )
34 11 27 33 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( X o. `' G ) ) .<_ W )
35 1 2 3 8 4 atmod4i2
 |-  ( ( K e. HL /\ ( ( G ` P ) e. A /\ ( R ` ( X o. `' G ) ) e. B /\ W e. B ) /\ ( R ` ( X o. `' G ) ) .<_ W ) -> ( ( ( G ` P ) ./\ W ) .\/ ( R ` ( X o. `' G ) ) ) = ( ( ( G ` P ) .\/ ( R ` ( X o. `' G ) ) ) ./\ W ) )
36 18 22 29 32 34 35 syl131anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) ./\ W ) .\/ ( R ` ( X o. `' G ) ) ) = ( ( ( G ` P ) .\/ ( R ` ( X o. `' G ) ) ) ./\ W ) )
37 hlol
 |-  ( K e. HL -> K e. OL )
38 18 37 syl
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. OL )
39 1 3 14 olj02
 |-  ( ( K e. OL /\ ( R ` ( X o. `' G ) ) e. B ) -> ( ( 0. ` K ) .\/ ( R ` ( X o. `' G ) ) ) = ( R ` ( X o. `' G ) ) )
40 38 29 39 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( 0. ` K ) .\/ ( R ` ( X o. `' G ) ) ) = ( R ` ( X o. `' G ) ) )
41 17 36 40 3eqtr3d
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) .\/ ( R ` ( X o. `' G ) ) ) ./\ W ) = ( R ` ( X o. `' G ) ) )
42 10 41 eqtrd
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ W ) = ( R ` ( X o. `' G ) ) )