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 ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
tendoi.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion tendoi2 ⊢ S ∈ E ∧ F ∈ T → I ⁡ S ⁡ F = S ⁡ F -1

Proof

Step Hyp Ref Expression
1 tendoi.i ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
2 tendoi.t ⊢ T = LTrn ⁡ K ⁡ W
3 1 2 tendoi ⊢ S ∈ E → I ⁡ S = g ∈ T ⟼ S ⁡ g -1
4 3 adantr ⊢ S ∈ E ∧ F ∈ T → I ⁡ S = g ∈ T ⟼ S ⁡ g -1
5 fveq2 ⊢ g = F → S ⁡ g = S ⁡ F
6 5 cnveqd ⊢ g = F → S ⁡ g -1 = S ⁡ F -1
7 6 adantl ⊢ S ∈ E ∧ F ∈ T ∧ g = F → S ⁡ g -1 = S ⁡ F -1
8 simpr ⊢ S ∈ E ∧ F ∈ T → F ∈ T
9 fvex ⊢ S ⁡ F ∈ V
10 9 cnvex ⊢ S ⁡ F -1 ∈ V
11 10 a1i ⊢ S ∈ E ∧ F ∈ T → S ⁡ F -1 ∈ V
12 4 7 8 11 fvmptd ⊢ S ∈ E ∧ F ∈ T → I ⁡ S ⁡ F = S ⁡ F -1