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	⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝐹 ) = ◡ ( 𝑆 ‘ 𝐹 ) )