Metamath Proof Explorer

Theorem cpmatelimp

Description: Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmat.s 
|- S = ( N ConstPolyMat R )
cpmat.p 
|- P = ( Poly1 ` R )
cpmat.c 
|- C = ( N Mat P )
cpmat.b 
|- B = ( Base ` C )
Assertion cpmatelimp 
|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmat.s 
 |-  S = ( N ConstPolyMat R )
2 cpmat.p 
 |-  P = ( Poly1 ` R )
3 cpmat.c 
 |-  C = ( N Mat P )
4 cpmat.b 
 |-  B = ( Base ` C )
5 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> M e. B )
6 5 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> M e. B )
7 1 2 3 4 cpmatel 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
8 7 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
9 8 biimpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. B ) -> ( M e. S -> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
10 9 impancom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> ( M e. B -> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
11 6 10 jcai 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> ( M e. B /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
12 11 ex 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) ) )