Theorem trlid0

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

	Ref	Expression
Hypotheses	trlid0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	trlid0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	trlid0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlid0.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlid0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		trlid0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		trlid0.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		trlid0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trlid0.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	5 6 3	lhpexnle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
8		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
10		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11	1 3 10	idltrn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
12	11	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
13		eqid	⊢ ( I ↾ 𝐵 ) = ( I ↾ 𝐵 )
14	1 5 6 3 10	ltrnideq	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ↔ ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 ) )
15	8 12 9 14	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ↔ ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 ) )
16	13 15	mpbii	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 )
17	5 2 6 3 10 4	trl0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 ) ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = 0 )
18	8 9 12 16 17	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = 0 )
19	7 18	rexlimddv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = 0 )