Metamath Proof Explorer

Theorem cdlemj2

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate p . (Contributed by NM, 20-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 )
Assertion cdlemj2 
|- ( ( ( ( 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 ) ) ) -> ( U ` h ) = ( V ` h ) )

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 simpl1 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( 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 ) ) )
7 simpl2 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) )
8 simpl3l 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` F ) =/= ( R ` g ) )
9 simpl3r 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` g ) =/= ( R ` h ) )
10 simpr 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) )
11 eqid 
 |-  ( le ` K ) = ( le ` K )
12 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
13 1 2 3 4 5 11 12 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) ) -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) )
14 6 7 8 9 10 13 syl113anc 
 |-  ( ( ( ( ( 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. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) )
15 14 exp32 
 |-  ( ( ( ( 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. ( Atoms ` K ) -> ( -. p ( le ` K ) W -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) ) ) )
16 15 ralrimiv 
 |-  ( ( ( ( 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 ) ) ) -> A. p e. ( Atoms ` K ) ( -. p ( le ` K ) W -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) ) )
17 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 ) ) ) -> ( K e. HL /\ W e. H ) )
18 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 ) ) ) -> U e. E )
19 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 ) ) ) -> h e. T )
20 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ h e. T ) -> ( U ` h ) e. T )
21 17 18 19 20 syl3anc 
 |-  ( ( ( ( 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 ) ) ) -> ( U ` h ) e. T )
22 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 ) ) ) -> V e. E )
23 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ h e. T ) -> ( V ` h ) e. T )
24 17 22 19 23 syl3anc 
 |-  ( ( ( ( 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 ) ) ) -> ( V ` h ) e. T )
25 11 12 2 3 ltrneq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U ` h ) e. T /\ ( V ` h ) e. T ) -> ( A. p e. ( Atoms ` K ) ( -. p ( le ` K ) W -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) ) <-> ( U ` h ) = ( V ` h ) ) )
26 17 21 24 25 syl3anc 
 |-  ( ( ( ( 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 ) ) ) -> ( A. p e. ( Atoms ` K ) ( -. p ( le ` K ) W -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) ) <-> ( U ` h ) = ( V ` h ) ) )
27 16 26 mpbid 
 |-  ( ( ( ( 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 ) ) ) -> ( U ` h ) = ( V ` h ) )