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

Metamath Proof Explorer

Theorem trlid0

Description: The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses trlid0.b 
|- B = ( Base ` K )
trlid0.z 
|- .0. = ( 0. ` K )
trlid0.h 
|- H = ( LHyp ` K )
trlid0.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlid0 
|- ( ( K e. HL /\ W e. H ) -> ( R ` ( _I |` B ) ) = .0. )

Proof

Step Hyp Ref Expression
1 trlid0.b 
 |-  B = ( Base ` K )
2 trlid0.z 
 |-  .0. = ( 0. ` K )
3 trlid0.h 
 |-  H = ( LHyp ` K )
4 trlid0.r 
 |-  R = ( ( trL ` K ) ` W )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 5 6 3 lhpexnle 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. ( Atoms ` K ) -. p ( le ` K ) W )
8 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
9 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) )
10 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
11 1 3 10 idltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. ( ( LTrn ` K ) ` W ) )
12 11 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( _I |` B ) e. ( ( LTrn ` K ) ` W ) )
13 eqid 
 |-  ( _I |` B ) = ( _I |` B )
14 1 5 6 3 10 ltrnideq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( _I |` B ) e. ( ( LTrn ` K ) ` W ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( _I |` B ) = ( _I |` B ) <-> ( ( _I |` B ) ` p ) = p ) )
15 8 12 9 14 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( _I |` B ) = ( _I |` B ) <-> ( ( _I |` B ) ` p ) = p ) )
16 13 15 mpbii 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( _I |` B ) ` p ) = p )
17 5 2 6 3 10 4 trl0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) /\ ( ( _I |` B ) e. ( ( LTrn ` K ) ` W ) /\ ( ( _I |` B ) ` p ) = p ) ) -> ( R ` ( _I |` B ) ) = .0. )
18 8 9 12 16 17 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` ( _I |` B ) ) = .0. )
19 7 18 rexlimddv 
 |-  ( ( K e. HL /\ W e. H ) -> ( R ` ( _I |` B ) ) = .0. )