Metamath Proof Explorer

Theorem decpmatmul

Description: The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power. (Contributed by AV, 21-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmatmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
decpmatmul.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
decpmatmul.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
decpmatmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion decpmatmul ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 decpmatmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 decpmatmul.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 decpmatmul.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 decpmatmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
5 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) )
6 oveq1 ⊢ ( 𝑥 = 𝑖 → ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) = ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) )
7 oveq2 ⊢ ( 𝑦 = 𝑗 → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) = ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) )
8 6 7 oveqan12d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) = ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) )
9 8 mpteq2dv ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) )
10 9 oveq2d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) )
11 10 mpteq2dv ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) )
12 11 oveq2d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
13 12 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
14 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
15 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
16 ovexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) ∈ V )
17 5 13 14 15 16 ovmpod ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) 𝑗 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
18 2 3 matrcl ⊢ ( 𝑈 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ V ) )
19 18 simpld ⊢ ( 𝑈 ∈ 𝐵 → 𝑁 ∈ Fin )
20 19 adantr ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → 𝑁 ∈ Fin )
21 20 anim2i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
22 21 ancomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23 22 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
24 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
25 4 24 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
26 23 25 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
27 26 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
28 27 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
29 28 eqcomd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
30 29 oveqd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) = ( ( 𝑈 decompPMat 𝑘 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) )
31 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ Ring )
34 33 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
35 34 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑅 ∈ Ring )
36 23 simpld ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ Fin )
37 36 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
38 37 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑁 ∈ Fin )
39 simpl2l ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑈 ∈ 𝐵 )
40 39 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑈 ∈ 𝐵 )
41 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝐾 ) → 𝑘 ∈ ℕ0 )
42 41 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑘 ∈ ℕ0 )
43 35 40 42 3jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) )
44 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
45 1 2 3 4 44 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
46 43 45 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
47 4 31 44 matbas2i ⊢ ( ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
48 46 47 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
49 simpl2r ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑊 ∈ 𝐵 )
50 49 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑊 ∈ 𝐵 )
51 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝐾 ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
52 51 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
53 35 50 52 3jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) )
54 1 2 3 4 44 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
55 53 54 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
56 4 31 44 matbas2i ⊢ ( ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
57 55 56 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
58 24 31 32 35 38 38 38 48 57 mamuval ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) )
59 30 58 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) )
60 59 mpteq2dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) )
61 60 oveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) )
62 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
63 ovexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0 ... 𝐾 ) ∈ V )
64 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
65 33 64 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ CMnd )
66 65 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ CMnd )
67 66 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑅 ∈ CMnd )
68 67 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
69 38 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑁 ∈ Fin )
70 35 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ Ring )
71 70 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → 𝑅 ∈ Ring )
72 simpl2 ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
73 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → 𝑡 ∈ 𝑁 )
74 43 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) )
75 74 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) )
76 75 45 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
77 4 31 44 72 73 76 matecld ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ∈ ( Base ‘ 𝑅 ) )
78 simpl3 ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
79 55 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
80 79 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
81 4 31 44 73 78 80 matecld ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
82 31 32 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
83 71 77 81 82 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑡 ∈ 𝑁 ) → ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
84 83 ralrimiva ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ∀ 𝑡 ∈ 𝑁 ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
85 31 68 69 84 gsummptcl ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
86 4 31 44 38 35 85 matbas2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
87 eqid ⊢ ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) )
88 fzfid ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0 ... 𝐾 ) ∈ Fin )
89 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ V ) → 𝑁 ∈ Fin )
90 89 89 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ V ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
91 18 90 syl ⊢ ( 𝑈 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
92 91 adantr ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
93 92 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
94 93 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
95 94 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
96 mpoexga ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ∈ V )
97 95 96 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ∈ V )
98 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝐴 ) ∈ V )
99 87 88 97 98 fsuppmptdm ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) finSupp ( 0g ‘ 𝐴 ) )
100 4 44 62 37 63 34 86 99 matgsum ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) )
101 61 100 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) )
102 101 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) = ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑥 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑦 ) ) ) ) ) ) ) 𝑗 ) )
103 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) )
104 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝐾 ∈ ℕ0 )
105 1 2 3 decpmatmullem ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) )
106 37 34 103 14 15 104 105 syl213anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) )
107 simpll1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑅 ∈ Ring )
108 simplrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑖 ∈ 𝑁 )
109 simprl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑡 ∈ 𝑁 )
110 3 eleq2i ⊢ ( 𝑈 ∈ 𝐵 ↔ 𝑈 ∈ ( Base ‘ 𝐶 ) )
111 110 biimpi ⊢ ( 𝑈 ∈ 𝐵 → 𝑈 ∈ ( Base ‘ 𝐶 ) )
112 111 adantr ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
113 112 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
114 113 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
115 114 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
116 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
117 2 116 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ∧ 𝑈 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) )
118 108 109 115 117 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) )
119 41 ad2antll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑘 ∈ ℕ0 )
120 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) = ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) )
121 120 116 1 31 coe1fvalcl ⊢ ( ( ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
122 118 119 121 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
123 simplrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑗 ∈ 𝑁 )
124 49 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑊 ∈ 𝐵 )
125 2 116 3 109 123 124 matecld ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝑡 𝑊 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
126 51 ad2antll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
127 eqid ⊢ ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) = ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) )
128 127 116 1 31 coe1fvalcl ⊢ ( ( ( 𝑡 𝑊 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
129 125 126 128 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
130 31 32 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
131 107 122 129 130 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
132 31 66 37 88 131 gsumcom3fi ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) )
133 14 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑖 ∈ 𝑁 )
134 133 anim1i ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ) )
135 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) = ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) )
136 43 134 135 syl2an2r ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) = ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) )
137 simplrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑗 ∈ 𝑁 )
138 137 anim1ci ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
139 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) = ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) )
140 53 138 139 syl2an2r ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) = ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) )
141 136 140 oveq12d ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) = ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) )
142 141 eqcomd ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) = ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) )
143 142 mpteq2dva ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) = ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) )
144 143 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) )
145 144 mpteq2dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) )
146 145 oveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
147 106 132 146 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
148 17 102 147 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) )
149 148 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) )
150 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
151 22 150 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐶 ∈ Ring )
152 simprl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑈 ∈ 𝐵 )
153 simprr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
154 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
155 3 154 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
156 151 152 153 155 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
157 156 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
158 1 2 3 4 44 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
159 157 158 syld3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
160 4 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
161 23 160 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐴 ∈ Ring )
162 ringcmn ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
163 161 162 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐴 ∈ CMnd )
164 fzfid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 0 ... 𝐾 ) ∈ Fin )
165 161 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝐴 ∈ Ring )
166 33 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑅 ∈ Ring )
167 simpl2l ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑈 ∈ 𝐵 )
168 41 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑘 ∈ ℕ0 )
169 166 167 168 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) )
170 169 45 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
171 simpl2r ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑊 ∈ 𝐵 )
172 51 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
173 166 171 172 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) )
174 173 54 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
175 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
176 44 175 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
177 165 170 174 176 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
178 177 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
179 44 163 164 178 gsummptcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
180 4 44 eqmat ⊢ ( ( ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) ) )
181 159 179 180 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) ) )
182 149 181 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) )