Metamath Proof Explorer

Theorem tendo0plr

Description: Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014)

Ref Expression
Hypotheses tendo0.b ⊢ B = Base K
tendo0.h ⊢ H = LHyp ⁡ K
tendo0.t ⊢ T = LTrn ⁡ K ⁡ W
tendo0.e ⊢ E = TEndo ⁡ K ⁡ W
tendo0.o ⊢ O = f ∈ T ⟼ I ↾ B
tendo0pl.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
Assertion tendo0plr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P O = S

Proof

Step Hyp Ref Expression
1 tendo0.b ⊢ B = Base K
2 tendo0.h ⊢ H = LHyp ⁡ K
3 tendo0.t ⊢ T = LTrn ⁡ K ⁡ W
4 tendo0.e ⊢ E = TEndo ⁡ K ⁡ W
5 tendo0.o ⊢ O = f ∈ T ⟼ I ↾ B
6 tendo0pl.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
7 1 2 3 4 5 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → O ∈ E
8 7 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → O ∈ E
9 2 3 4 6 tendoplcom ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ O ∈ E → S P O = O P S
10 8 9 mpd3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P O = O P S
11 1 2 3 4 5 6 tendo0pl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → O P S = S
12 10 11 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P O = S