Metamath Proof Explorer

Theorem cdlemg44

Description: Part of proof of Lemma G of Crawley p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (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 )
Assertion cdlemg44 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) = ( G o. F ) )

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 eqid 
 |-  ( le ` K ) = ( le ` K )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 4 5 1 lhpexnle 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. ( Atoms ` K ) -. p ( le ` K ) W )
7 6 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> E. p e. ( Atoms ` K ) -. p ( le ` K ) W )
8 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( K e. HL /\ W e. H ) )
9 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> F e. T )
10 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> G e. T )
11 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
12 8 9 10 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( F o. G ) e. T )
13 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ F e. T ) -> ( G o. F ) e. T )
14 8 10 9 13 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( G o. F ) e. T )
15 3simpc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) )
16 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( R ` F ) =/= ( R ` G ) )
17 1 2 3 4 5 cdlemg44b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F ` ( G ` p ) ) = ( G ` ( F ` p ) ) )
18 8 9 10 15 16 17 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( F ` ( G ` p ) ) = ( G ` ( F ` p ) ) )
19 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( F e. T /\ G e. T ) )
20 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> p e. ( Atoms ` K ) )
21 4 5 1 2 ltrncoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ p e. ( Atoms ` K ) ) -> ( ( F o. G ) ` p ) = ( F ` ( G ` p ) ) )
22 8 19 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( ( F o. G ) ` p ) = ( F ` ( G ` p ) ) )
23 4 5 1 2 ltrncoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ F e. T ) /\ p e. ( Atoms ` K ) ) -> ( ( G o. F ) ` p ) = ( G ` ( F ` p ) ) )
24 8 10 9 20 23 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( ( G o. F ) ` p ) = ( G ` ( F ` p ) ) )
25 18 22 24 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( ( F o. G ) ` p ) = ( ( G o. F ) ` p ) )
26 4 5 1 2 cdlemd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T /\ ( G o. F ) e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) /\ ( ( F o. G ) ` p ) = ( ( G o. F ) ` p ) ) -> ( F o. G ) = ( G o. F ) )
27 8 12 14 15 25 26 syl311anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) /\ p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) -> ( F o. G ) = ( G o. F ) )
28 27 rexlimdv3a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( E. p e. ( Atoms ` K ) -. p ( le ` K ) W -> ( F o. G ) = ( G o. F ) ) )
29 7 28 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) = ( G o. F ) )