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 ‘ ( 𝑡 𝑊 𝐽 ) ) ‘ ( 𝐾𝑙 ) ) ) ) ) ) ) )