Metamath Proof Explorer

Theorem decpmatmullem

Description: Lemma for decpmatmul . (Contributed by AV, 20-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmatmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
decpmatmul.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
decpmatmul.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion decpmatmullem ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝐽 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 decpmatmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 decpmatmul.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 decpmatmul.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
5 4 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑅 ∈ Ring )
6 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐶 ∈ Ring )
8 simpl ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → 𝑈 ∈ 𝐵 )
9 8 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑈 ∈ 𝐵 )
10 simpr ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → 𝑊 ∈ 𝐵 )
11 10 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
12 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
13 3 12 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
14 7 9 11 13 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
15 14 3adant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 )
16 simp33 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐾 ∈ ℕ0 )
17 3simpa ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
18 17 3ad2ant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
19 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝐽 ) = ( ( coe1 ‘ ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) ) ‘ 𝐾 ) )
20 5 15 16 18 19 syl31anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝐽 ) = ( ( coe1 ‘ ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) ) ‘ 𝐾 ) )
21 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
22 eqid ⊢ ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
23 2 22 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐶 ) )
24 23 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( .r ‘ 𝐶 ) = ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
25 21 24 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( .r ‘ 𝐶 ) = ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
26 25 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( .r ‘ 𝐶 ) = ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
27 26 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) = ( 𝑈 ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑊 ) )
28 27 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) = ( 𝐼 ( 𝑈 ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑊 ) 𝐽 ) )
29 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
30 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
31 21 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
32 31 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑃 ∈ Ring )
33 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
34 33 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑁 ∈ Fin )
35 2 29 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐶 ) )
36 3 35 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐵 = ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
37 21 36 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐵 = ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
38 37 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑈 ∈ 𝐵 ↔ 𝑈 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
39 38 biimpcd ⊢ ( 𝑈 ∈ 𝐵 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
40 39 adantr ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
41 40 impcom ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑈 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
42 41 3adant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑈 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
43 21 35 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐶 ) )
44 3 43 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐵 = ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
45 44 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑊 ∈ 𝐵 ↔ 𝑊 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
46 45 biimpcd ⊢ ( 𝑊 ∈ 𝐵 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑊 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
47 46 adantl ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑊 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
48 47 impcom ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
49 48 3adant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑊 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
50 simp31 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐼 ∈ 𝑁 )
51 simp32 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐽 ∈ 𝑁 )
52 22 29 30 32 34 34 34 42 49 50 51 mamufv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( 𝑈 ( 𝑃 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑊 ) 𝐽 ) = ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) )
53 28 52 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) = ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) )
54 53 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( coe1 ‘ ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) ) )
55 54 fveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝐼 ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) 𝐽 ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) ) ‘ 𝐾 ) )
56 32 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝑃 ∈ Ring )
57 50 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
58 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝑡 ∈ 𝑁 )
59 simpl2l ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝑈 ∈ 𝐵 )
60 2 29 3 57 58 59 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝐼 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) )
61 51 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
62 simpl2r ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝑊 ∈ 𝐵 )
63 2 29 3 58 61 62 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑡 𝑊 𝐽 ) ∈ ( Base ‘ 𝑃 ) )
64 29 30 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐼 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑡 𝑊 𝐽 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ∈ ( Base ‘ 𝑃 ) )
65 56 60 63 64 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ∈ ( Base ‘ 𝑃 ) )
66 65 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ∀ 𝑡 ∈ 𝑁 ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ∈ ( Base ‘ 𝑃 ) )
67 1 29 5 16 66 34 coe1fzgsumd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ‘ 𝐾 ) ) ) )
68 simpl1r ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝑅 ∈ Ring )
69 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
70 1 30 69 29 coe1mul ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 𝑈 𝑡 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑡 𝑊 𝐽 ) ∈ ( Base ‘ 𝑃 ) ) → ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ) )
71 68 60 63 70 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ) )
72 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 0 ... 𝑘 ) = ( 0 ... 𝐾 ) )
73 fvoveq1 ⊢ ( 𝑘 = 𝐾 → ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) = ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) )
74 73 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) = ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) )
75 72 74 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) )
76 75 oveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) )
77 76 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) ∧ 𝑘 = 𝐾 ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) )
78 16 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → 𝐾 ∈ ℕ0 )
79 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ∈ V )
80 71 77 78 79 fvmptd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑡 ∈ 𝑁 ) → ( ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) )
81 80 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑡 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ‘ 𝐾 ) ) = ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ) )
82 81 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ) ) )
83 67 82 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑡 ∈ 𝑁 ↦ ( ( 𝐼 𝑈 𝑡 ) ( .r ‘ 𝑃 ) ( 𝑡 𝑊 𝐽 ) ) ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ) ) )
84 20 55 83 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝐼 ( ( 𝑈 ( .r ‘ 𝐶 ) 𝑊 ) decompPMat 𝐾 ) 𝐽 ) = ( 𝑅 Σg ( 𝑡 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝐾 ) ↦ ( ( ( coe1 ‘ ( 𝐼 𝑈 𝑡 ) ) ‘ 𝑙 ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾 − 𝑙 ) ) ) ) ) ) ) )