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 ⊢ 𝐵 = ( 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 )