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 birani ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
112 111 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
113 112 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
114 113 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐶 ) )
115 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
116 2 115 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ∧ 𝑈 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) )
117 108 109 114 116 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) )
118 41 ad2antll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑘 ∈ ℕ0 )
119 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) = ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) )
120 119 115 1 31 coe1fvalcl ⊢ ( ( ( 𝑖 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
121 117 118 120 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
122 simplrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑗 ∈ 𝑁 )
123 49 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → 𝑊 ∈ 𝐵 )
124 2 115 3 109 122 123 matecld ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝑡 𝑊 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
125 51 ad2antll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
126 eqid ⊢ ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) = ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) )
127 126 115 1 31 coe1fvalcl ⊢ ( ( ( 𝑡 𝑊 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
128 124 125 127 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
129 31 32 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
130 107 121 128 129 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
131 31 66 37 88 130 gsumcom3fi ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) )
132 14 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑖 ∈ 𝑁 )
133 132 anim1i ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ) )
134 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑡 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) = ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) )
135 43 133 134 syl2an2r ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) = ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) )
136 simplrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑗 ∈ 𝑁 )
137 136 anim1ci ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
138 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) ∧ ( 𝑡 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) = ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) )
139 53 137 138 syl2an2r ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) = ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) )
140 135 139 oveq12d ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) = ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) )
141 140 eqcomd ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) = ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) )
142 141 mpteq2dva ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) = ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) )
143 142 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) )
144 143 mpteq2dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) )
145 144 oveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( ( coe1 ‘ ( 𝑖 𝑈 𝑡 ) ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝑗 ) ) ‘ ( 𝐾 − 𝑘 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
146 106 131 145 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑈 decompPMat 𝑘 ) 𝑡 ) ( .r ‘ 𝑅 ) ( 𝑡 ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) 𝑗 ) ) ) ) ) ) )
147 17 102 146 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) )
148 147 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) )
149 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
150 22 149 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐶 ∈ Ring )
151 simprl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑈 ∈ 𝐵 )
152 simprr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
153 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
154 3 153 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
155 150 151 152 154 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
156 155 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
157 1 2 3 4 44 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
158 156 157 syld3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
159 4 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
160 23 159 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐴 ∈ Ring )
161 ringcmn ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
162 160 161 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐴 ∈ CMnd )
163 fzfid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 0 ... 𝐾 ) ∈ Fin )
164 160 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝐴 ∈ Ring )
165 33 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑅 ∈ Ring )
166 simpl2l ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑈 ∈ 𝐵 )
167 41 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑘 ∈ ℕ0 )
168 165 166 167 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) )
169 168 45 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
170 simpl2r ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → 𝑊 ∈ 𝐵 )
171 51 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝐾 − 𝑘 ) ∈ ℕ0 )
172 165 170 171 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐵 ∧ ( 𝐾 − 𝑘 ) ∈ ℕ0 ) )
173 172 54 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) )
174 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
175 44 174 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑈 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
176 164 169 173 175 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
177 176 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ∈ ( Base ‘ 𝐴 ) )
178 44 162 163 177 gsummptcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
179 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 ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) ) )
180 158 178 179 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝑗 ) = ( 𝑖 ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) 𝑗 ) ) )
181 148 180 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝐾 ) ↦ ( ( 𝑈 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑊 decompPMat ( 𝐾 − 𝑘 ) ) ) ) ) )