Metamath Proof Explorer

Theorem cdleml1N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleml1.b 
|- B = ( Base ` K )
cdleml1.h 
|- H = ( LHyp ` K )
cdleml1.t 
|- T = ( ( LTrn ` K ) ` W )
cdleml1.r 
|- R = ( ( trL ` K ) ` W )
cdleml1.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion cdleml1N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( U ` f ) ) = ( R ` ( V ` f ) ) )

Proof

Step Hyp Ref Expression
1 cdleml1.b 
 |-  B = ( Base ` K )
2 cdleml1.h 
 |-  H = ( LHyp ` K )
3 cdleml1.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 cdleml1.r 
 |-  R = ( ( trL ` K ) ` W )
5 cdleml1.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( K e. HL /\ W e. H ) )
7 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> U e. E )
8 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> f e. T )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 9 2 3 4 5 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ f e. T ) -> ( R ` ( U ` f ) ) ( le ` K ) ( R ` f ) )
11 6 7 8 10 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( U ` f ) ) ( le ` K ) ( R ` f ) )
12 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> K e. HL )
13 hlatl 
 |-  ( K e. HL -> K e. AtLat )
14 12 13 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> K e. AtLat )
15 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ f e. T ) -> ( U ` f ) e. T )
16 6 7 8 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( U ` f ) e. T )
17 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( U ` f ) =/= ( _I |` B ) )
18 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
19 1 18 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U ` f ) e. T /\ ( U ` f ) =/= ( _I |` B ) ) -> ( R ` ( U ` f ) ) e. ( Atoms ` K ) )
20 6 16 17 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( U ` f ) ) e. ( Atoms ` K ) )
21 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> f =/= ( _I |` B ) )
22 1 18 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ f =/= ( _I |` B ) ) -> ( R ` f ) e. ( Atoms ` K ) )
23 6 8 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` f ) e. ( Atoms ` K ) )
24 9 18 atcmp 
 |-  ( ( K e. AtLat /\ ( R ` ( U ` f ) ) e. ( Atoms ` K ) /\ ( R ` f ) e. ( Atoms ` K ) ) -> ( ( R ` ( U ` f ) ) ( le ` K ) ( R ` f ) <-> ( R ` ( U ` f ) ) = ( R ` f ) ) )
25 14 20 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( ( R ` ( U ` f ) ) ( le ` K ) ( R ` f ) <-> ( R ` ( U ` f ) ) = ( R ` f ) ) )
26 11 25 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( U ` f ) ) = ( R ` f ) )
27 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> V e. E )
28 9 2 3 4 5 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ f e. T ) -> ( R ` ( V ` f ) ) ( le ` K ) ( R ` f ) )
29 6 27 8 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( V ` f ) ) ( le ` K ) ( R ` f ) )
30 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ f e. T ) -> ( V ` f ) e. T )
31 6 27 8 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( V ` f ) e. T )
32 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( V ` f ) =/= ( _I |` B ) )
33 1 18 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( V ` f ) e. T /\ ( V ` f ) =/= ( _I |` B ) ) -> ( R ` ( V ` f ) ) e. ( Atoms ` K ) )
34 6 31 32 33 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( V ` f ) ) e. ( Atoms ` K ) )
35 9 18 atcmp 
 |-  ( ( K e. AtLat /\ ( R ` ( V ` f ) ) e. ( Atoms ` K ) /\ ( R ` f ) e. ( Atoms ` K ) ) -> ( ( R ` ( V ` f ) ) ( le ` K ) ( R ` f ) <-> ( R ` ( V ` f ) ) = ( R ` f ) ) )
36 14 34 23 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( ( R ` ( V ` f ) ) ( le ` K ) ( R ` f ) <-> ( R ` ( V ` f ) ) = ( R ` f ) ) )
37 29 36 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( V ` f ) ) = ( R ` f ) )
38 26 37 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> ( R ` ( U ` f ) ) = ( R ` ( V ` f ) ) )