Metamath Proof Explorer

Theorem m2cpminvid2lem

Description: Lemma for m2cpminvid2 . (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

Ref Expression
Hypotheses m2cpminvid2lem.s 
|- S = ( N ConstPolyMat R )
m2cpminvid2lem.p 
|- P = ( Poly1 ` R )
Assertion m2cpminvid2lem 
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. n e. NN0 ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )

Proof

Step Hyp Ref Expression
1 m2cpminvid2lem.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpminvid2lem.p 
 |-  P = ( Poly1 ` R )
3 eqid 
 |-  ( N Mat P ) = ( N Mat P )
4 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
5 1 2 3 4 cpmatelimp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. ( Base ` ( N Mat P ) ) /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) ) )
6 5 3impia 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( M e. ( Base ` ( N Mat P ) ) /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
7 6 simprd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) )
8 7 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) )
9 fvoveq1 
 |-  ( i = x -> ( coe1 ` ( i M j ) ) = ( coe1 ` ( x M j ) ) )
10 9 fveq1d 
 |-  ( i = x -> ( ( coe1 ` ( i M j ) ) ` k ) = ( ( coe1 ` ( x M j ) ) ` k ) )
11 10 eqeq1d 
 |-  ( i = x -> ( ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) <-> ( ( coe1 ` ( x M j ) ) ` k ) = ( 0g ` R ) ) )
12 11 ralbidv 
 |-  ( i = x -> ( A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) <-> A. k e. NN ( ( coe1 ` ( x M j ) ) ` k ) = ( 0g ` R ) ) )
13 oveq2 
 |-  ( j = y -> ( x M j ) = ( x M y ) )
14 13 fveq2d 
 |-  ( j = y -> ( coe1 ` ( x M j ) ) = ( coe1 ` ( x M y ) ) )
15 14 fveq1d 
 |-  ( j = y -> ( ( coe1 ` ( x M j ) ) ` k ) = ( ( coe1 ` ( x M y ) ) ` k ) )
16 15 eqeq1d 
 |-  ( j = y -> ( ( ( coe1 ` ( x M j ) ) ` k ) = ( 0g ` R ) <-> ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) ) )
17 16 ralbidv 
 |-  ( j = y -> ( A. k e. NN ( ( coe1 ` ( x M j ) ) ` k ) = ( 0g ` R ) <-> A. k e. NN ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) ) )
18 12 17 rspc2v 
 |-  ( ( x e. N /\ y e. N ) -> ( A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) -> A. k e. NN ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) ) )
19 18 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) -> A. k e. NN ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) ) )
20 fveqeq2 
 |-  ( k = n -> ( ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) <-> ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) )
21 20 cbvralvw 
 |-  ( A. k e. NN ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) <-> A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) )
22 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> R e. Ring )
23 eqid 
 |-  ( Base ` P ) = ( Base ` P )
24 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> x e. N )
25 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> y e. N )
26 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> M e. ( Base ` ( N Mat P ) ) )
27 26 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> M e. ( Base ` ( N Mat P ) ) )
28 3 23 4 24 25 27 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( x M y ) e. ( Base ` P ) )
29 0nn0 
 |-  0 e. NN0
30 eqid 
 |-  ( coe1 ` ( x M y ) ) = ( coe1 ` ( x M y ) )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 30 23 2 31 coe1fvalcl 
 |-  ( ( ( x M y ) e. ( Base ` P ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) )
33 28 29 32 sylancl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) )
34 22 33 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) )
35 34 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) )
36 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
37 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
38 2 36 31 37 coe1scl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) -> ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) )
39 35 38 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) )
40 39 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) ` n ) )
41 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) = ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) )
42 eqeq1 
 |-  ( l = n -> ( l = 0 <-> n = 0 ) )
43 42 ifbid 
 |-  ( l = n -> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) = if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) )
44 43 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) /\ l = n ) -> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) = if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) )
45 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
46 45 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> n e. NN0 )
47 fvex 
 |-  ( ( coe1 ` ( x M y ) ) ` 0 ) e. _V
48 fvex 
 |-  ( 0g ` R ) e. _V
49 47 48 ifex 
 |-  if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) e. _V
50 49 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) e. _V )
51 41 44 46 50 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( ( l e. NN0 |-> if ( l = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) ) ` n ) = if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) )
52 nnne0 
 |-  ( n e. NN -> n =/= 0 )
53 52 neneqd 
 |-  ( n e. NN -> -. n = 0 )
54 53 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> -. n = 0 )
55 54 iffalsed 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> if ( n = 0 , ( ( coe1 ` ( x M y ) ) ` 0 ) , ( 0g ` R ) ) = ( 0g ` R ) )
56 40 51 55 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( 0g ` R ) )
57 eqcom 
 |-  ( ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) <-> ( 0g ` R ) = ( ( coe1 ` ( x M y ) ) ` n ) )
58 57 biimpi 
 |-  ( ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) -> ( 0g ` R ) = ( ( coe1 ` ( x M y ) ) ` n ) )
59 56 58 sylan9eq 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) /\ ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )
60 59 ex 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ n e. NN ) -> ( ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) ) )
61 60 ralimdva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) ) )
62 61 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )
63 34 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) -> ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) )
64 2 36 31 ply1sclid 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) = ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) )
65 64 eqcomd 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) )
66 63 65 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) )
67 62 66 jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) /\ A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) ) -> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
68 67 ex 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. n e. NN ( ( coe1 ` ( x M y ) ) ` n ) = ( 0g ` R ) -> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
69 21 68 syl5bi 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. k e. NN ( ( coe1 ` ( x M y ) ) ` k ) = ( 0g ` R ) -> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
70 19 69 syld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) -> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
71 8 70 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
72 c0ex 
 |-  0 e. _V
73 fveq2 
 |-  ( n = 0 -> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) )
74 fveq2 
 |-  ( n = 0 -> ( ( coe1 ` ( x M y ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` 0 ) )
75 73 74 eqeq12d 
 |-  ( n = 0 -> ( ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) <-> ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
76 75 ralunsn 
 |-  ( 0 e. _V -> ( A. n e. ( NN u. { 0 } ) ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) <-> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
77 72 76 mp1i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( A. n e. ( NN u. { 0 } ) ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) <-> ( A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) /\ ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
78 71 77 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. n e. ( NN u. { 0 } ) ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )
79 df-n0 
 |-  NN0 = ( NN u. { 0 } )
80 79 raleqi 
 |-  ( A. n e. NN0 ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) <-> A. n e. ( NN u. { 0 } ) ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )
81 78 80 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. n e. NN0 ( ( coe1 ` ( ( algSc ` P ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )