Metamath Proof Explorer

Theorem pm2mpmhmlem2

Description: Lemma 2 for pm2mpmhm . (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpmhm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pm2mpmhm.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpmhm.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpmhm.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
pm2mpmhm.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
pm2mpmhm.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion pm2mpmhmlem2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 pm2mpmhm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pm2mpmhm.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpmhm.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 pm2mpmhm.q ⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
5 pm2mpmhm.t ⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
6 pm2mpmhm.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
7 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
8 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
9 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ Ring )
11 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
12 11 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
13 simpr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
14 13 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
15 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
16 6 15 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
17 10 12 14 16 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
18 eqid ⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 )
19 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
20 eqid ⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 )
21 1 2 6 18 19 20 3 4 5 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
22 7 8 17 21 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
23 1 2 6 3 decpmatmul ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) = ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) )
24 23 ad4ant234 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) = ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) )
25 24 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) = ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) )
26 25 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) )
27 26 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
28 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
29 3 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
30 29 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ Ring )
31 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
32 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
33 ringcmn ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
34 29 33 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ CMnd )
35 34 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ CMnd )
36 fzfid ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
37 30 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝐴 ∈ Ring )
38 simp-5r ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
39 12 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑥 ∈ 𝐵 )
40 elfznn0 ⊢ ( 𝑧 ∈ ( 0 ... 𝑘 ) → 𝑧 ∈ ℕ0 )
41 40 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑧 ∈ ℕ0 )
42 1 2 6 3 31 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ ℕ0 ) → ( 𝑥 decompPMat 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
43 38 39 41 42 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑥 decompPMat 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
44 14 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑦 ∈ 𝐵 )
45 fznn0sub ⊢ ( 𝑧 ∈ ( 0 ... 𝑘 ) → ( 𝑘 − 𝑧 ) ∈ ℕ0 )
46 45 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑧 ) ∈ ℕ0 )
47 1 2 6 3 31 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑘 − 𝑧 ) ∈ ℕ0 ) → ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ∈ ( Base ‘ 𝐴 ) )
48 38 44 46 47 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ∈ ( Base ‘ 𝐴 ) )
49 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
50 31 49 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑥 decompPMat 𝑧 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ∈ ( Base ‘ 𝐴 ) )
51 37 43 48 50 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ∈ ( Base ‘ 𝐴 ) )
52 51 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑧 ∈ ( 0 ... 𝑘 ) ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ∈ ( Base ‘ 𝐴 ) )
53 31 35 36 52 gsummptcl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
54 53 ralrimiva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
55 1 2 6 3 49 32 decpmatmulsumfsupp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ) finSupp ( 0g ‘ 𝐴 ) )
56 55 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ) finSupp ( 0g ‘ 𝐴 ) )
57 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
58 4 28 20 19 30 31 18 32 54 56 57 gsummoncoe1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑛 ) = ⦋ 𝑛 / 𝑘 ⦌ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) )
59 csbov2g ⊢ ( 𝑛 ∈ ℕ0 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) = ( 𝐴 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) )
60 id ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
61 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 0 ... 𝑘 ) = ( 0 ... 𝑛 ) )
62 oveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 − 𝑧 ) = ( 𝑛 − 𝑧 ) )
63 62 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) = ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) )
64 63 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) = ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) )
65 61 64 mpteq12dv ⊢ ( 𝑘 = 𝑛 → ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) )
66 65 adantl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑘 = 𝑛 ) → ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) )
67 60 66 csbied ⊢ ( 𝑛 ∈ ℕ0 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) )
68 67 oveq2d ⊢ ( 𝑛 ∈ ℕ0 → ( 𝐴 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) = ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) ) )
69 59 68 eqtrd ⊢ ( 𝑛 ∈ ℕ0 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) = ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) ) )
70 69 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ⦋ 𝑛 / 𝑘 ⦌ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) = ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) ) )
71 eqidd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) = ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) )
72 oveq2 ⊢ ( 𝑟 = 𝑛 → ( 0 ... 𝑟 ) = ( 0 ... 𝑛 ) )
73 fvoveq1 ⊢ ( 𝑟 = 𝑛 → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) )
74 73 oveq2d ⊢ ( 𝑟 = 𝑛 → ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) = ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) )
75 72 74 mpteq12dv ⊢ ( 𝑟 = 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) )
76 75 oveq2d ⊢ ( 𝑟 = 𝑛 → ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) = ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
77 76 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑟 = 𝑛 ) → ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) = ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
78 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) ) ∈ V )
79 71 77 57 78 fvmptd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) ‘ 𝑛 ) = ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
80 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
81 4 ply1ring ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
82 29 81 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
83 ringcmn ⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ CMnd )
84 82 83 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ CMnd )
85 84 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑄 ∈ CMnd )
86 nn0ex ⊢ ℕ0 ∈ V
87 86 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ℕ0 ∈ V )
88 11 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) )
89 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) )
90 88 89 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) )
91 90 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) )
92 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
93 91 92 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
94 93 fmpttd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑄 ) )
95 1 2 6 18 19 20 3 4 pm2mpghmlem2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
96 91 95 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
97 28 80 85 87 94 96 gsumcl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
98 13 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) )
99 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) )
100 98 99 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
101 100 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
102 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
103 101 102 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
104 103 fmpttd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑄 ) )
105 7 8 14 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
106 105 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
107 1 2 6 18 19 20 3 4 pm2mpghmlem2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
108 106 107 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
109 28 80 85 87 104 108 gsumcl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
110 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
111 4 110 49 28 coe1mul ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ) → ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) = ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) )
112 111 fveq1d ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ) → ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) = ( ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) ‘ 𝑛 ) )
113 30 97 109 112 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) = ( ( 𝑟 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑟 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑟 − 𝑙 ) ) ) ) ) ) ‘ 𝑛 ) )
114 oveq2 ⊢ ( 𝑧 = 𝑙 → ( 𝑥 decompPMat 𝑧 ) = ( 𝑥 decompPMat 𝑙 ) )
115 oveq2 ⊢ ( 𝑧 = 𝑙 → ( 𝑛 − 𝑧 ) = ( 𝑛 − 𝑙 ) )
116 115 oveq2d ⊢ ( 𝑧 = 𝑙 → ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) = ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) )
117 114 116 oveq12d ⊢ ( 𝑧 = 𝑙 → ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) = ( ( 𝑥 decompPMat 𝑙 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) ) )
118 117 cbvmptv ⊢ ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑙 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) ) )
119 29 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝐴 ∈ Ring )
120 simp-5r ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
121 12 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 ∈ 𝐵 )
122 simpr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
123 1 2 6 3 31 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
124 120 121 122 123 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
125 124 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑥 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
126 8 12 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) )
127 126 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) )
128 1 2 6 3 32 decpmatfsupp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
129 127 128 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
130 elfznn0 ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → 𝑙 ∈ ℕ0 )
131 130 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝑙 ∈ ℕ0 )
132 4 28 20 19 119 31 18 32 125 129 131 gsummoncoe1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) = ⦋ 𝑙 / 𝑘 ⦌ ( 𝑥 decompPMat 𝑘 ) )
133 csbov2g ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ⦋ 𝑙 / 𝑘 ⦌ ( 𝑥 decompPMat 𝑘 ) = ( 𝑥 decompPMat ⦋ 𝑙 / 𝑘 ⦌ 𝑘 ) )
134 csbvarg ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ⦋ 𝑙 / 𝑘 ⦌ 𝑘 = 𝑙 )
135 134 oveq2d ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑥 decompPMat ⦋ 𝑙 / 𝑘 ⦌ 𝑘 ) = ( 𝑥 decompPMat 𝑙 ) )
136 133 135 eqtrd ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ⦋ 𝑙 / 𝑘 ⦌ ( 𝑥 decompPMat 𝑘 ) = ( 𝑥 decompPMat 𝑙 ) )
137 136 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ⦋ 𝑙 / 𝑘 ⦌ ( 𝑥 decompPMat 𝑘 ) = ( 𝑥 decompPMat 𝑙 ) )
138 132 137 eqtr2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑥 decompPMat 𝑙 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) )
139 14 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑦 ∈ 𝐵 )
140 1 2 6 3 31 decpmatcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
141 120 139 122 140 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
142 141 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑦 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
143 8 14 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
144 143 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) )
145 1 2 6 3 32 decpmatfsupp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
146 144 145 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
147 fznn0sub ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑙 ) ∈ ℕ0 )
148 147 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛 − 𝑙 ) ∈ ℕ0 )
149 4 28 20 19 119 31 18 32 142 146 148 gsummoncoe1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) = ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ ( 𝑦 decompPMat 𝑘 ) )
150 ovex ⊢ ( 𝑛 − 𝑙 ) ∈ V
151 csbov2g ⊢ ( ( 𝑛 − 𝑙 ) ∈ V → ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ ( 𝑦 decompPMat 𝑘 ) = ( 𝑦 decompPMat ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ 𝑘 ) )
152 150 151 mp1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ ( 𝑦 decompPMat 𝑘 ) = ( 𝑦 decompPMat ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ 𝑘 ) )
153 csbvarg ⊢ ( ( 𝑛 − 𝑙 ) ∈ V → ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ 𝑘 = ( 𝑛 − 𝑙 ) )
154 150 153 mp1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ 𝑘 = ( 𝑛 − 𝑙 ) )
155 154 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑦 decompPMat ⦋ ( 𝑛 − 𝑙 ) / 𝑘 ⦌ 𝑘 ) = ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) )
156 149 152 155 3eqtrrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) )
157 138 156 oveq12d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑥 decompPMat 𝑙 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) ) = ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) )
158 157 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑙 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) )
159 118 158 syl5eq ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) )
160 159 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) ) = ( 𝐴 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑙 ) ( .r ‘ 𝐴 ) ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
161 79 113 160 3eqtr4rd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑧 ) ) ) ) ) = ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) )
162 58 70 161 3eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) )
163 162 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) )
164 29 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐴 ∈ Ring )
165 84 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑄 ∈ CMnd )
166 86 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ℕ0 ∈ V )
167 4 ply1lmod ⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
168 29 167 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
169 168 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑄 ∈ LMod )
170 34 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ CMnd )
171 fzfid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
172 29 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝐴 ∈ Ring )
173 simp-4r ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
174 simplrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 ∈ 𝐵 )
175 174 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑥 ∈ 𝐵 )
176 40 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑧 ∈ ℕ0 )
177 173 175 176 42 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑥 decompPMat 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
178 simplrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑦 ∈ 𝐵 )
179 178 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → 𝑦 ∈ 𝐵 )
180 45 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑧 ) ∈ ℕ0 )
181 173 179 180 47 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ∈ ( Base ‘ 𝐴 ) )
182 172 177 181 50 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ∈ ( Base ‘ 𝐴 ) )
183 182 ralrimiva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑧 ∈ ( 0 ... 𝑘 ) ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ∈ ( Base ‘ 𝐴 ) )
184 31 170 171 183 gsummptcl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ∈ ( Base ‘ 𝐴 ) )
185 29 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ Ring )
186 4 ply1sca ⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
187 185 186 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
188 187 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( Scalar ‘ 𝑄 ) = 𝐴 )
189 188 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ 𝐴 ) )
190 184 189 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
191 eqid ⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
192 4 20 191 19 28 ply1moncl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ∈ ( Base ‘ 𝑄 ) )
193 185 192 sylancom ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ∈ ( Base ‘ 𝑄 ) )
194 eqid ⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
195 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
196 28 194 18 195 lmodvscl ⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
197 169 190 193 196 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
198 197 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑄 ) )
199 1 2 6 18 19 20 3 4 28 5 pm2mpmhmlem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
200 28 80 165 166 198 199 gsumcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
201 82 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑄 ∈ Ring )
202 90 92 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
203 202 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑄 ) )
204 90 95 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
205 28 80 165 166 203 204 gsumcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
206 100 102 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ∈ ( Base ‘ 𝑄 ) )
207 206 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑄 ) )
208 7 8 14 107 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) finSupp ( 0g ‘ 𝑄 ) )
209 28 80 165 166 207 208 gsumcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
210 28 110 ringcl ⊢ ( ( 𝑄 ∈ Ring ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
211 201 205 209 210 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) )
212 eqid ⊢ ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
213 eqid ⊢ ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) = ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) )
214 4 28 212 213 ply1coe1eq ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ∧ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ∈ ( Base ‘ 𝑄 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) ↔ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) )
215 164 200 211 214 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) ‘ 𝑛 ) ↔ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) ) )
216 163 215 mpbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 Σg ( 𝑧 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝑥 decompPMat 𝑧 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑘 − 𝑧 ) ) ) ) ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) )
217 22 27 216 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) )
218 1 2 6 18 19 20 3 4 5 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
219 7 8 12 218 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
220 1 2 6 18 19 20 3 4 5 pm2mpfval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
221 7 8 14 220 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
222 219 221 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑥 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ( .r ‘ 𝑄 ) ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑦 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑄 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) )
223 217 222 eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) )
224 223 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) )