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 β€˜ 𝐢 ) )