Metamath Proof Explorer

Theorem tendoipl2

Description: Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014)

Ref Expression
Hypotheses tendoicl.h ⊢ H = LHyp ⁡ K
tendoicl.t ⊢ T = LTrn ⁡ K ⁡ W
tendoicl.e ⊢ E = TEndo ⁡ K ⁡ W
tendoicl.i ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
tendoi.b ⊢ B = Base K
tendoi.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
tendoi.o ⊢ O = f ∈ T ⟼ I ↾ B
Assertion tendoipl2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P I ⁡ S = O

Proof

Step Hyp Ref Expression
1 tendoicl.h ⊢ H = LHyp ⁡ K
2 tendoicl.t ⊢ T = LTrn ⁡ K ⁡ W
3 tendoicl.e ⊢ E = TEndo ⁡ K ⁡ W
4 tendoicl.i ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
5 tendoi.b ⊢ B = Base K
6 tendoi.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
7 tendoi.o ⊢ O = f ∈ T ⟼ I ↾ B
8 1 2 3 4 tendoicl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → I ⁡ S ∈ E
9 1 2 3 6 tendoplcom ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ I ⁡ S ∈ E → S P I ⁡ S = I ⁡ S P S
10 8 9 mpd3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P I ⁡ S = I ⁡ S P S
11 1 2 3 4 5 6 7 tendoipl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → I ⁡ S P S = O
12 10 11 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S P I ⁡ S = O