Theorem tendo0co2

Description: The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 ? (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendo0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tendo0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	tendo0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	tendo0co2	⊢ ( ( ( 𝐾 ∈ 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	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
7	5 1	tendo02	⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 → ( 𝑂 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( I ↾ 𝐵 ) )
8	6 7	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( I ↾ 𝐵 ) )
9	5 1	tendo02	⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
10	9	3ad2ant2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
11	5 1	tendo02	⊢ ( 𝐺 ∈ 𝑇 → ( 𝑂 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
12	11	3ad2ant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑂 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
13	10 12	coeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑂 ‘ 𝐹 ) ∘ ( 𝑂 ‘ 𝐺 ) ) = ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) )
14		f1oi	⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
15		f1of	⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
16		fcoi1	⊢ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
17	14 15 16	mp2b	⊢ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 )
18	13 17	eqtr2di	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( I ↾ 𝐵 ) = ( ( 𝑂 ‘ 𝐹 ) ∘ ( 𝑂 ‘ 𝐺 ) ) )
19	8 18	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑂 ‘ 𝐹 ) ∘ ( 𝑂 ‘ 𝐺 ) ) )