Theorem tendo0plr

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

	Ref	Expression
Hypotheses	tendo0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tendo0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	tendo0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	tendo0pl.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion	tendo0plr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 𝑃 𝑂 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		tendo0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tendo0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		tendo0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		tendo0.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5		tendo0.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6		tendo0pl.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
7	1 2 3 4 5	tendo0cl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
8	7	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → 𝑂 ∈ 𝐸 )
9	2 3 4 6	tendoplcom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑂 ∈ 𝐸 ) → ( 𝑆 𝑃 𝑂 ) = ( 𝑂 𝑃 𝑆 ) )
10	8 9	mpd3an3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 𝑃 𝑂 ) = ( 𝑂 𝑃 𝑆 ) )
11	1 2 3 4 5 6	tendo0pl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑂 𝑃 𝑆 ) = 𝑆 )
12	10 11	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 𝑃 𝑂 ) = 𝑆 )