Metamath Proof Explorer

Theorem cdlemj1

Description: Part of proof of Lemma J of Crawley p. 118. (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses cdlemj.b 
|- B = ( Base ` K )
cdlemj.h 
|- H = ( LHyp ` K )
cdlemj.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemj.r 
|- R = ( ( trL ` K ) ` W )
cdlemj.e 
|- E = ( ( TEndo ` K ) ` W )
cdlemj.l 
|- .<_ = ( le ` K )
cdlemj.a 
|- A = ( Atoms ` K )
Assertion cdlemj1 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) )

Proof

Step Hyp Ref Expression
1 cdlemj.b 
 |-  B = ( Base ` K )
2 cdlemj.h 
 |-  H = ( LHyp ` K )
3 cdlemj.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 cdlemj.r 
 |-  R = ( ( trL ` K ) ` W )
5 cdlemj.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 cdlemj.l 
 |-  .<_ = ( le ` K )
7 cdlemj.a 
 |-  A = ( Atoms ` K )
8 simp123 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( U ` F ) = ( V ` F ) )
9 8 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` F ) ` p ) = ( ( V ` F ) ` p ) )
10 9 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) = ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) )
11 10 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) )
12 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( K e. HL /\ W e. H ) )
13 simp131 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> F e. T )
14 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> g e. T )
15 simp121 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> U e. E )
16 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( p e. A /\ -. p .<_ W ) )
17 simp132 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> F =/= ( _I |` B ) )
18 simp23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> g =/= ( _I |` B ) )
19 simp31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( R ` F ) =/= ( R ` g ) )
20 eqid 
 |-  ( join ` K ) = ( join ` K )
21 eqid 
 |-  ( meet ` K ) = ( meet ` K )
22 eqid 
 |-  ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) )
23 1 6 20 21 7 2 3 4 5 22 cdlemi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ g e. T ) /\ ( U e. E /\ ( p e. A /\ -. p .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ g =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` g ) ) ) -> ( ( U ` g ) ` p ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) )
24 12 13 14 15 16 17 18 19 23 syl323anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` g ) ` p ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( U ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) )
25 simp122 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> V e. E )
26 eqid 
 |-  ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) )
27 1 6 20 21 7 2 3 4 5 26 cdlemi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ g e. T ) /\ ( V e. E /\ ( p e. A /\ -. p .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ g =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` g ) ) ) -> ( ( V ` g ) ` p ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) )
28 12 13 14 25 16 17 18 19 27 syl323anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( V ` g ) ` p ) = ( ( p ( join ` K ) ( R ` g ) ) ( meet ` K ) ( ( ( V ` F ) ` p ) ( join ` K ) ( R ` ( g o. `' F ) ) ) ) )
29 11 24 28 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` g ) ` p ) = ( ( V ` g ) ` p ) )
30 29 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) = ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) )
31 30 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) )
32 simp133 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> h e. T )
33 simp21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> h =/= ( _I |` B ) )
34 simp32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( R ` g ) =/= ( R ` h ) )
35 eqid 
 |-  ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) )
36 1 6 20 21 7 2 3 4 5 35 cdlemi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ h e. T ) /\ ( U e. E /\ ( p e. A /\ -. p .<_ W ) ) /\ ( g =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` g ) =/= ( R ` h ) ) ) -> ( ( U ` h ) ` p ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) )
37 12 14 32 15 16 18 33 34 36 syl323anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` h ) ` p ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( U ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) )
38 eqid 
 |-  ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) )
39 1 6 20 21 7 2 3 4 5 38 cdlemi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ h e. T ) /\ ( V e. E /\ ( p e. A /\ -. p .<_ W ) ) /\ ( g =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` g ) =/= ( R ` h ) ) ) -> ( ( V ` h ) ` p ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) )
40 12 14 32 25 16 18 33 34 39 syl323anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( V ` h ) ` p ) = ( ( p ( join ` K ) ( R ` h ) ) ( meet ` K ) ( ( ( V ` g ) ` p ) ( join ` K ) ( R ` ( h o. `' g ) ) ) ) )
41 31 37 40 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) )