Metamath Proof Explorer

Theorem tendoex

Description: Generalization of Lemma K of Crawley p. 118, cdlemk . TODO: can this be used to shorten uses of cdlemk ? (Contributed by NM, 15-Oct-2013)

Ref Expression
Hypotheses tendoex.l 
|- .<_ = ( le ` K )
tendoex.h 
|- H = ( LHyp ` K )
tendoex.t 
|- T = ( ( LTrn ` K ) ` W )
tendoex.r 
|- R = ( ( trL ` K ) ` W )
tendoex.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion tendoex 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> E. u e. E ( u ` F ) = N )

Proof

Step Hyp Ref Expression
1 tendoex.l 
 |-  .<_ = ( le ` K )
2 tendoex.h 
 |-  H = ( LHyp ` K )
3 tendoex.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoex.r 
 |-  R = ( ( trL ` K ) ` W )
5 tendoex.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> K e. HL )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 6 7 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> K e. OP )
9 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( K e. HL /\ W e. H ) )
10 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> N e. T )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 2 3 4 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T ) -> ( R ` N ) e. ( Base ` K ) )
13 9 10 12 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( R ` N ) e. ( Base ` K ) )
14 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( R ` F ) e. ( Atoms ` K ) )
15 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( R ` N ) .<_ ( R ` F ) )
16 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
17 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
18 11 1 16 17 leat 
 |-  ( ( ( K e. OP /\ ( R ` N ) e. ( Base ` K ) /\ ( R ` F ) e. ( Atoms ` K ) ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) )
19 8 13 14 15 18 syl31anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) )
20 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( R ` N ) .<_ ( R ` F ) )
21 breq2 
 |-  ( ( R ` F ) = ( 0. ` K ) -> ( ( R ` N ) .<_ ( R ` F ) <-> ( R ` N ) .<_ ( 0. ` K ) ) )
22 20 21 syl5ibcom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( ( R ` F ) = ( 0. ` K ) -> ( R ` N ) .<_ ( 0. ` K ) ) )
23 22 imp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` N ) .<_ ( 0. ` K ) )
24 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> K e. HL )
25 24 7 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> K e. OP )
26 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( K e. HL /\ W e. H ) )
27 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> N e. T )
28 26 27 12 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` N ) e. ( Base ` K ) )
29 11 1 16 ople0 
 |-  ( ( K e. OP /\ ( R ` N ) e. ( Base ` K ) ) -> ( ( R ` N ) .<_ ( 0. ` K ) <-> ( R ` N ) = ( 0. ` K ) ) )
30 25 28 29 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( ( R ` N ) .<_ ( 0. ` K ) <-> ( R ` N ) = ( 0. ` K ) ) )
31 23 30 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( R ` N ) = ( 0. ` K ) )
32 31 olcd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) /\ ( R ` F ) = ( 0. ` K ) ) -> ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) )
33 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( K e. HL /\ W e. H ) )
34 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> F e. T )
35 16 17 2 3 4 trlator0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. ( Atoms ` K ) \/ ( R ` F ) = ( 0. ` K ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( ( R ` F ) e. ( Atoms ` K ) \/ ( R ` F ) = ( 0. ` K ) ) )
37 19 32 36 mpjaodan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) )
38 37 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) .<_ ( R ` F ) ) -> ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) )
39 eqcom 
 |-  ( ( R ` N ) = ( R ` F ) <-> ( R ` F ) = ( R ` N ) )
40 2 3 4 5 cdlemk 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> E. u e. E ( u ` F ) = N )
41 40 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` F ) = ( R ` N ) ) -> E. u e. E ( u ` F ) = N )
42 39 41 sylan2b 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( R ` F ) ) -> E. u e. E ( u ` F ) = N )
43 eqid 
 |-  ( h e. T |-> ( _I |` ( Base ` K ) ) ) = ( h e. T |-> ( _I |` ( Base ` K ) ) )
44 11 2 3 5 43 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> ( h e. T |-> ( _I |` ( Base ` K ) ) ) e. E )
45 44 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> ( h e. T |-> ( _I |` ( Base ` K ) ) ) e. E )
46 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> F e. T )
47 43 11 tendo02 
 |-  ( F e. T -> ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) = ( _I |` ( Base ` K ) ) )
48 46 47 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) = ( _I |` ( Base ` K ) ) )
49 11 16 2 3 4 trlid0b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T ) -> ( N = ( _I |` ( Base ` K ) ) <-> ( R ` N ) = ( 0. ` K ) ) )
50 49 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) -> ( N = ( _I |` ( Base ` K ) ) <-> ( R ` N ) = ( 0. ` K ) ) )
51 50 biimpar 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> N = ( _I |` ( Base ` K ) ) )
52 48 51 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) = N )
53 fveq1 
 |-  ( u = ( h e. T |-> ( _I |` ( Base ` K ) ) ) -> ( u ` F ) = ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) )
54 53 eqeq1d 
 |-  ( u = ( h e. T |-> ( _I |` ( Base ` K ) ) ) -> ( ( u ` F ) = N <-> ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) = N ) )
55 54 rspcev 
 |-  ( ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) e. E /\ ( ( h e. T |-> ( _I |` ( Base ` K ) ) ) ` F ) = N ) -> E. u e. E ( u ` F ) = N )
56 45 52 55 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) = ( 0. ` K ) ) -> E. u e. E ( u ` F ) = N )
57 42 56 jaodan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( ( R ` N ) = ( R ` F ) \/ ( R ` N ) = ( 0. ` K ) ) ) -> E. u e. E ( u ` F ) = N )
58 38 57 syldan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) ) /\ ( R ` N ) .<_ ( R ` F ) ) -> E. u e. E ( u ` F ) = N )
59 58 3impa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` N ) .<_ ( R ` F ) ) -> E. u e. E ( u ` F ) = N )