Metamath Proof Explorer


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 ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) → ( 𝑂 ‘ ( 𝐹𝐺 ) ) = ( ( 𝑂𝐹 ) ∘ ( 𝑂𝐺 ) ) )