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. )