This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemn3

Description: Part of proof of Lemma N of Crawley p. 121 line 31. (Contributed by NM, 21-Feb-2014)

Ref Expression
Hypotheses cdlemn3.l 
|- .<_ = ( le ` K )
cdlemn3.a 
|- A = ( Atoms ` K )
cdlemn3.p 
|- P = ( ( oc ` K ) ` W )
cdlemn3.h 
|- H = ( LHyp ` K )
cdlemn3.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemn3.f 
|- F = ( iota_ h e. T ( h ` P ) = Q )
cdlemn3.g 
|- G = ( iota_ h e. T ( h ` P ) = R )
cdlemn3.j 
|- J = ( iota_ h e. T ( h ` Q ) = R )
Assertion cdlemn3 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) = G )

Proof

Step Hyp Ref Expression
1 cdlemn3.l 
 |-  .<_ = ( le ` K )
2 cdlemn3.a 
 |-  A = ( Atoms ` K )
3 cdlemn3.p 
 |-  P = ( ( oc ` K ) ` W )
4 cdlemn3.h 
 |-  H = ( LHyp ` K )
5 cdlemn3.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 cdlemn3.f 
 |-  F = ( iota_ h e. T ( h ` P ) = Q )
7 cdlemn3.g 
 |-  G = ( iota_ h e. T ( h ` P ) = R )
8 cdlemn3.j 
 |-  J = ( iota_ h e. T ( h ` Q ) = R )
9 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( K e. HL /\ W e. H ) )
10 1 2 4 3 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
11 10 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
12 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
13 1 2 4 5 6 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T )
14 9 11 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F e. T )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 15 4 5 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
17 9 14 16 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
18 f1of 
 |-  ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> F : ( Base ` K ) --> ( Base ` K ) )
19 17 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F : ( Base ` K ) --> ( Base ` K ) )
20 11 simpld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> P e. A )
21 15 2 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
22 20 21 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> P e. ( Base ` K ) )
23 fvco3 
 |-  ( ( F : ( Base ` K ) --> ( Base ` K ) /\ P e. ( Base ` K ) ) -> ( ( J o. F ) ` P ) = ( J ` ( F ` P ) ) )
24 19 22 23 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( J o. F ) ` P ) = ( J ` ( F ` P ) ) )
25 1 2 4 5 6 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q )
26 9 11 12 25 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( F ` P ) = Q )
27 26 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J ` ( F ` P ) ) = ( J ` Q ) )
28 1 2 4 5 8 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J ` Q ) = R )
29 24 27 28 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( J o. F ) ` P ) = R )
30 1 2 4 5 7 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( G ` P ) = R )
31 11 30 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( G ` P ) = R )
32 29 31 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( J o. F ) ` P ) = ( G ` P ) )
33 1 2 4 5 8 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> J e. T )
34 4 5 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ J e. T /\ F e. T ) -> ( J o. F ) e. T )
35 9 33 14 34 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) e. T )
36 1 2 4 5 7 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> G e. T )
37 11 36 syld3an2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> G e. T )
38 1 2 4 5 ltrneq3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( J o. F ) e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( J o. F ) ` P ) = ( G ` P ) <-> ( J o. F ) = G ) )
39 9 35 37 11 38 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( ( J o. F ) ` P ) = ( G ` P ) <-> ( J o. F ) = G ) )
40 32 39 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) = G )