Metamath Proof Explorer

Theorem cpmatelimp2

Description: Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-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 )
cpmatel2.k 
|- K = ( Base ` R )
cpmatel2.a 
|- A = ( algSc ` P )
Assertion cpmatelimp2 
|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) ) )

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 cpmatel2.k 
 |-  K = ( Base ` R )
6 cpmatel2.a 
 |-  A = ( algSc ` P )
7 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> M e. B )
8 7 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> M e. B )
9 1 2 3 4 5 6 cpmatel2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
10 9 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
11 10 biimpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. B ) -> ( M e. S -> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
12 11 impancom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> ( M e. B -> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
13 8 12 jcai 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> ( M e. B /\ A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
14 13 ex 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) ) )