Metamath Proof Explorer

Theorem istendo

Description: The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in Crawley p. 117, penultimate line. (Contributed by NM, 8-Jun-2013)

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

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 1 2 3 4 5 tendoset ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )
7 6 eleq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 ↔ 𝑆 ∈ { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } ) )
8 3 fvexi ⊢ 𝑇 ∈ V
9 fex ⊢ ( ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ 𝑇 ∈ V ) → 𝑆 ∈ V )
10 8 9 mpan2 ⊢ ( 𝑆 : 𝑇 ⟶ 𝑇 → 𝑆 ∈ V )
11 10 3ad2ant1 ⊢ ( ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) → 𝑆 ∈ V )
12 feq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 : 𝑇 ⟶ 𝑇 ↔ 𝑆 : 𝑇 ⟶ 𝑇 ) )
13 fveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) )
14 fveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑓 ) )
15 fveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ 𝑔 ) = ( 𝑆 ‘ 𝑔 ) )
16 14 15 coeq12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
17 13 16 eqeq12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ) )
18 17 2ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ) )
19 14 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) )
20 19 breq1d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ↔ ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
21 20 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ↔ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
22 12 18 21 3anbi123d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ) )
23 11 22 elab3 ⊢ ( 𝑆 ∈ { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
24 7 23 bitrdi ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑆 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ) )