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 → U P V ⁡ 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 → U P V ⁡ F = U ⁡ F ∘ V ⁡ F
6 5 3expa ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F
7 6 3adant1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ 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 → U P V ⁡ F ∈ T