Metamath Proof Explorer

Theorem tendoplass

Description: The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion tendoplass ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) = ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → 𝑆 ∈ 𝐸 )
7 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → 𝑈 ∈ 𝐸 )
8 1 2 3 4 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑆 𝑃 𝑈 ) ∈ 𝐸 )
9 5 6 7 8 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑆 𝑃 𝑈 ) ∈ 𝐸 )
10 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → 𝑉 ∈ 𝐸 )
11 1 2 3 4 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 𝑃 𝑈 ) ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ∈ 𝐸 )
12 5 9 10 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ∈ 𝐸 )
13 1 2 3 4 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 )
14 5 7 10 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 )
15 1 2 3 4 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 ) → ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ∈ 𝐸 )
16 5 6 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ∈ 𝐸 )
17 coass ⊢ ( ( ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑈 ‘ 𝑔 ) ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
18 simplr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → 𝑆 ∈ 𝐸 )
19 simplr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → 𝑈 ∈ 𝐸 )
20 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ 𝑇 )
21 4 2 tendopl2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑈 ‘ 𝑔 ) ) )
22 18 19 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑈 ‘ 𝑔 ) ) )
23 22 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑈 ‘ 𝑔 ) ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
24 simplr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → 𝑉 ∈ 𝐸 )
25 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
26 19 24 20 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
27 26 coeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
28 17 23 27 3eqtr4a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) ) )
29 9 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 𝑃 𝑈 ) ∈ 𝐸 )
30 4 2 tendopl2 ⊢ ( ( ( 𝑆 𝑃 𝑈 ) ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
31 29 24 20 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( ( 𝑆 𝑃 𝑈 ) ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
32 14 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 )
33 4 2 tendopl2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ‘ 𝑔 ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) ) )
34 18 32 20 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ‘ 𝑔 ) = ( ( 𝑆 ‘ 𝑔 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) ) )
35 28 31 34 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ‘ 𝑔 ) )
36 35 ralrimiva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ∀ 𝑔 ∈ 𝑇 ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ‘ 𝑔 ) )
37 1 2 3 tendoeq1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ∈ 𝐸 ∧ ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ∈ 𝐸 ) ∧ ∀ 𝑔 ∈ 𝑇 ( ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) ‘ 𝑔 ) ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) = ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) )
38 5 12 16 36 37 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) = ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) )