Metamath Proof Explorer

Theorem pmatcollpw2lem

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

Ref Expression
Hypotheses pmatcollpw1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpw1.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw1.m ⊢ × = ( ·𝑠 ‘ 𝑃 )
pmatcollpw1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion pmatcollpw2lem ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pmatcollpw1.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pmatcollpw1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pmatcollpw1.m ⊢ × = ( ·𝑠 ‘ 𝑃 )
5 pmatcollpw1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6 pmatcollpw1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
8 mpoexga ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ∈ V )
9 7 7 8 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ∈ V )
10 9 ralrimivw ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ ℕ0 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ∈ V )
11 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) )
12 11 fnmpt ⊢ ( ∀ 𝑛 ∈ ℕ0 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ∈ V → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) Fn ℕ0 )
13 10 12 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) Fn ℕ0 )
14 nn0ex ⊢ ℕ0 ∈ V
15 14 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ℕ0 ∈ V )
16 fvexd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ 𝐶 ) ∈ V )
17 suppvalfn ⊢ ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ ( 0g ‘ 𝐶 ) ∈ V ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) supp ( 0g ‘ 𝐶 ) ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) } )
18 13 15 16 17 syl3anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) supp ( 0g ‘ 𝐶 ) ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) } )
19 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20 1 2 3 19 pmatcoe1fsupp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
21 oveq1 ⊢ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) × ( 𝑥 ↑ 𝑋 ) ) )
22 4 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → × = ( ·𝑠 ‘ 𝑃 ) )
23 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
24 23 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
25 24 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
26 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑥 ↑ 𝑋 ) = ( 𝑥 ↑ 𝑋 ) )
27 22 25 26 oveq123d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) × ( 𝑥 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) )
28 27 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 0g ‘ 𝑅 ) × ( 𝑥 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) )
29 24 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
30 29 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
31 30 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ 𝑅 ) )
32 31 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) )
33 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑅 ∈ Ring )
34 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
35 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
36 1 6 34 5 35 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
37 36 3ad2antl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
38 33 37 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
39 38 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
40 39 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
41 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
42 1 35 41 19 ply10s0 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
43 40 42 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
44 28 32 43 3eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 0g ‘ 𝑅 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
45 21 44 sylan9eqr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
46 45 ex ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
47 46 anasss ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) → ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
48 47 ralimdvva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
49 48 imim2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
50 49 ralimdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
51 50 reximdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
52 20 51 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
53 simpl3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
54 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
55 33 53 54 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0 ) )
56 1 2 3 decpmate ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) )
57 55 56 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) )
58 57 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) )
59 58 eqeq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
60 59 2ralbidva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
61 60 imbi2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
62 61 ralbidva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
63 62 rexbidv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
64 52 63 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
65 eqid ⊢ 𝑁 = 𝑁
66 65 biantrur ⊢ ( ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
67 65 biantrur ⊢ ( ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ↔ ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
68 67 bicomi ⊢ ( ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
69 68 ralbii ⊢ ( ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
70 66 69 bitr3i ⊢ ( ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
71 70 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
72 71 imbi2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) ↔ ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
73 72 rexralbidv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
74 64 73 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) )
75 mpoeq123 ⊢ ( ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) )
76 75 imim2i ⊢ ( ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) → ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) )
77 76 ralimi ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) )
78 77 reximi ⊢ ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑁 = 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 ( 𝑁 = 𝑁 ∧ ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) )
79 74 78 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) )
80 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) )
81 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑀 decompPMat 𝑛 ) = ( 𝑀 decompPMat 𝑥 ) )
82 81 oveqd ⊢ ( 𝑛 = 𝑥 → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) = ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) )
83 oveq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 ↑ 𝑋 ) = ( 𝑥 ↑ 𝑋 ) )
84 82 83 oveq12d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) = ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) )
85 84 mpoeq3dv ⊢ ( 𝑛 = 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) )
86 85 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑛 = 𝑥 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) )
87 id ⊢ ( 𝑁 ∈ Fin → 𝑁 ∈ Fin )
88 87 ancri ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
89 88 3ad2ant1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
90 89 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) )
91 mpoexga ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) ∈ V )
92 90 91 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) ∈ V )
93 80 86 54 92 fvmptd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) )
94 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
95 94 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
96 95 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
97 96 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
98 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
99 2 98 mat0op ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( 0g ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) )
100 97 99 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 0g ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) )
101 93 100 eqeq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ↔ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) )
102 101 imbi2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) ↔ ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) ) )
103 102 ralbidva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) ) )
104 103 rexbidv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑥 ) 𝑗 ) × ( 𝑥 ↑ 𝑋 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) ) ) )
105 79 104 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) )
106 nne ⊢ ( ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ↔ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) )
107 106 imbi2i ⊢ ( ( 𝑦 < 𝑥 → ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ) ↔ ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) )
108 107 ralbii ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) )
109 108 rexbii ⊢ ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ) ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝐶 ) ) )
110 105 109 sylibr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ) )
111 rabssnn0fi ⊢ ( { 𝑥 ∈ ℕ0 ∣ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) } ∈ Fin ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ¬ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) ) )
112 110 111 sylibr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { 𝑥 ∈ ℕ0 ∣ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐶 ) } ∈ Fin )
113 18 112 eqeltrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) supp ( 0g ‘ 𝐶 ) ) ∈ Fin )
114 funmpt ⊢ Fun ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) )
115 14 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ∈ V
116 funisfsupp ⊢ ( ( Fun ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ∧ ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ∈ V ∧ ( 0g ‘ 𝐶 ) ∈ V ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) ↔ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) supp ( 0g ‘ 𝐶 ) ) ∈ Fin ) )
117 114 115 16 116 mp3an12i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) ↔ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) supp ( 0g ‘ 𝐶 ) ) ∈ Fin ) )
118 113 117 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) )