This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istendod

Description: Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses tendoset.l ⊢ ≤ = ( le ‘ 𝐾 )
tendoset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
tendoset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
istendod.1 ⊢ ( 𝜑 → ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) )
istendod.2 ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ 𝑇 )
istendod.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
istendod.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) )
Assertion istendod ( 𝜑 → 𝑆 ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 tendoset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 tendoset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 tendoset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 istendod.1 ⊢ ( 𝜑 → ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) )
7 istendod.2 ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ 𝑇 )
8 istendod.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
9 istendod.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) )
10 8 3expb ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
11 10 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
12 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) )
13 1 2 3 4 5 istendo ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ) )
14 6 13 syl ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ) )
15 7 11 12 14 mpbir3and ⊢ ( 𝜑 → 𝑆 ∈ 𝐸 )