Metamath Proof Explorer

Theorem cdlemg44b

Description: Eliminate ( FP ) =/= P , ( GP ) =/= P from cdlemg44a . (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg44.h 
|- H = ( LHyp ` K )
cdlemg44.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemg44.r 
|- R = ( ( trL ` K ) ` W )
cdlemg44.l 
|- .<_ = ( le ` K )
cdlemg44.a 
|- A = ( Atoms ` K )
Assertion cdlemg44b 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg44.h 
 |-  H = ( LHyp ` K )
2 cdlemg44.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 cdlemg44.r 
 |-  R = ( ( trL ` K ) ` W )
4 cdlemg44.l 
 |-  .<_ = ( le ` K )
5 cdlemg44.a 
 |-  A = ( Atoms ` K )
6 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( K e. HL /\ W e. H ) )
7 simpl21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> F e. T )
8 simpl23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( P e. A /\ -. P .<_ W ) )
9 simpl22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> G e. T )
10 4 5 1 2 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
11 6 9 8 10 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
12 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( F ` P ) = P )
13 4 5 1 2 ltrnateq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) /\ ( F ` P ) = P ) -> ( F ` ( G ` P ) ) = ( G ` P ) )
14 6 7 8 11 12 13 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( F ` ( G ` P ) ) = ( G ` P ) )
15 12 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( G ` ( F ` P ) ) = ( G ` P ) )
16 14 15 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( F ` P ) = P ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
17 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( G ` P ) = P )
18 17 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( F ` ( G ` P ) ) = ( F ` P ) )
19 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( K e. HL /\ W e. H ) )
20 simpl22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> G e. T )
21 simpl23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( P e. A /\ -. P .<_ W ) )
22 simpl21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> F e. T )
23 4 5 1 2 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
24 19 22 21 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
25 4 5 1 2 ltrnateq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) /\ ( G ` P ) = P ) -> ( G ` ( F ` P ) ) = ( F ` P ) )
26 19 20 21 24 17 25 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( G ` ( F ` P ) ) = ( F ` P ) )
27 18 26 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( G ` P ) = P ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
28 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( K e. HL /\ W e. H ) )
29 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) )
30 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( F ` P ) =/= P )
31 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( G ` P ) =/= P )
32 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( R ` F ) =/= ( R ` G ) )
33 1 2 3 4 5 cdlemg44a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
34 28 29 30 31 32 33 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
35 16 27 34 pm2.61da2ne 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )