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 ∈ HL ∧ W ∈ 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 ⊢ ≤ K = ≤ K
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 5 6 3 lhpexnle ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ Atoms ⁡ K ¬ p ≤ K W
8 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → K ∈ HL ∧ W ∈ H
9 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W
10 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
11 1 3 10 idltrn ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∈ LTrn ⁡ K ⁡ W
12 11 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → I ↾ B ∈ LTrn ⁡ K ⁡ W
13 eqid ⊢ I ↾ B = I ↾ B
14 1 5 6 3 10 ltrnideq ⊢ K ∈ HL ∧ W ∈ H ∧ I ↾ B ∈ LTrn ⁡ K ⁡ W ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → I ↾ B = I ↾ B ↔ I ↾ B ⁡ p = p
15 8 12 9 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → I ↾ B = I ↾ B ↔ I ↾ B ⁡ p = p
16 13 15 mpbii ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → I ↾ B ⁡ p = p
17 5 2 6 3 10 4 trl0 ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W ∧ I ↾ B ∈ LTrn ⁡ K ⁡ W ∧ I ↾ B ⁡ p = p → R ⁡ I ↾ B = 0 ˙
18 8 9 12 16 17 syl112anc ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ K W → R ⁡ I ↾ B = 0 ˙
19 7 18 rexlimddv ⊢ K ∈ HL ∧ W ∈ H → R ⁡ I ↾ B = 0 ˙