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 ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐸𝑈𝐸𝑉𝐸 ) ) → ( ( 𝑆 𝑃 𝑈 ) 𝑃 𝑉 ) = ( 𝑆 𝑃 ( 𝑈 𝑃 𝑉 ) ) )