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