Metamath Proof Explorer

Theorem tendovalco

Description: Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses tendof.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendof.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendof.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendovalco ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 tendof.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendof.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendof.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 4 1 2 5 3 istendo ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) ) )
7 coeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 ) )
8 7 fveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) )
9 fveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝐹 ) )
10 9 coeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ) )
12 coeq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐺 ) )
13 12 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) )
14 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝑆 ‘ 𝑔 ) = ( 𝑆 ‘ 𝐺 ) )
15 14 coeq2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) )
16 13 15 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
17 11 16 rspc2v ⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
18 17 com12 ⊢ ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
19 18 3ad2ant2 ⊢ ( ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
20 6 19 syl6bi ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) )
21 20 3impia ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
22 21 imp ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) )