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

Metamath Proof Explorer

Theorem trlid0b

Description: A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013)

Ref Expression
Hypotheses trlid0b.b ⊢ B = Base K
trlid0b.z ⊢ 0 ˙ = 0. ⁡ K
trlid0b.h ⊢ H = LHyp ⁡ K
trlid0b.t ⊢ T = LTrn ⁡ K ⁡ W
trlid0b.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlid0b ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F = I ↾ B ↔ R ⁡ F = 0 ˙

Proof

Step Hyp Ref Expression
1 trlid0b.b ⊢ B = Base K
2 trlid0b.z ⊢ 0 ˙ = 0. ⁡ K
3 trlid0b.h ⊢ H = LHyp ⁡ K
4 trlid0b.t ⊢ T = LTrn ⁡ K ⁡ W
5 trlid0b.r ⊢ R = trL ⁡ K ⁡ W
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 1 6 3 4 5 trlnidatb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F ≠ I ↾ B ↔ R ⁡ F ∈ Atoms ⁡ K
8 2 6 3 4 5 trlatn0 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ Atoms ⁡ K ↔ R ⁡ F ≠ 0 ˙
9 7 8 bitrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F ≠ I ↾ B ↔ R ⁡ F ≠ 0 ˙
10 9 necon4bid ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F = I ↾ B ↔ R ⁡ F = 0 ˙