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

Metamath Proof Explorer

Theorem tendoi2

Description: Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013)

Ref Expression
Hypotheses tendoi.i ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
tendoi.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendoi2 ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝐹 ) = ◡ ( 𝑆 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tendoi.i ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
2 tendoi.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 tendoi ⊢ ( 𝑆 ∈ 𝐸 → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )
4 3 adantr ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )
5 fveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝑆 ‘ 𝑔 ) = ( 𝑆 ‘ 𝐹 ) )
6 5 cnveqd ⊢ ( 𝑔 = 𝐹 → ◡ ( 𝑆 ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝐹 ) )
7 6 adantl ⊢ ( ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 = 𝐹 ) → ◡ ( 𝑆 ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝐹 ) )
8 simpr ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
9 fvex ⊢ ( 𝑆 ‘ 𝐹 ) ∈ V
10 9 cnvex ⊢ ◡ ( 𝑆 ‘ 𝐹 ) ∈ V
11 10 a1i ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) ∈ V )
12 4 7 8 11 fvmptd ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝐹 ) = ◡ ( 𝑆 ‘ 𝐹 ) )