Metamath Proof Explorer

Theorem tendoplcl2

Description: Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses tendopl.h ⊢H=LHyp⁡K
tendopl.t ⊢T=LTrn⁡K⁡W
tendopl.e ⊢E=TEndo⁡K⁡W
tendopl.p ⊢P=s∈E,t∈E⟼f∈T⟼s⁡f∘t⁡f
Assertion tendoplcl2 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→UPV⁡F∈T

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢H=LHyp⁡K
2 tendopl.t ⊢T=LTrn⁡K⁡W
3 tendopl.e ⊢E=TEndo⁡K⁡W
4 tendopl.p ⊢P=s∈E,t∈E⟼f∈T⟼s⁡f∘t⁡f
5 4 2 tendopl2 ⊢U∈E∧V∈E∧F∈T→UPV⁡F=U⁡F∘V⁡F
6 5 3expa ⊢U∈E∧V∈E∧F∈T→UPV⁡F=U⁡F∘V⁡F
7 6 3adant1 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→UPV⁡F=U⁡F∘V⁡F
8 simp1 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→K∈HL∧W∈H
9 1 2 3 tendocl ⊢K∈HL∧W∈H∧U∈E∧F∈T→U⁡F∈T
10 9 3adant2r ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→U⁡F∈T
11 1 2 3 tendocl ⊢K∈HL∧W∈H∧V∈E∧F∈T→V⁡F∈T
12 11 3adant2l ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→V⁡F∈T
13 1 2 ltrnco ⊢K∈HL∧W∈H∧U⁡F∈T∧V⁡F∈T→U⁡F∘V⁡F∈T
14 8 10 12 13 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→U⁡F∘V⁡F∈T
15 7 14 eqeltrd ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T→UPV⁡F∈T