Metamath Proof Explorer

Theorem cpmatel2

Description: Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019) (Proof shortened by AV, 27-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	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 ) ) )

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	cpmatel	\|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. l e. NN ( ( coe1 ` ( i M j ) ) ` l ) = ( 0g ` R ) ) )
8		simpl2	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
9		eqid	\|- ( Base ` P ) = ( Base ` P )
10		simprl	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
11		simprr	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
12		simpl3	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> M e. B )
13	3 9 4 10 11 12	matecld	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` P ) )
14		eqid	\|- ( 0g ` R ) = ( 0g ` R )
15	5 14 2 9 6	cply1coe0bi	\|- ( ( R e. Ring /\ ( i M j ) e. ( Base ` P ) ) -> ( E. k e. K ( i M j ) = ( A ` k ) <-> A. l e. NN ( ( coe1 ` ( i M j ) ) ` l ) = ( 0g ` R ) ) )
16	8 13 15	syl2anc	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( E. k e. K ( i M j ) = ( A ` k ) <-> A. l e. NN ( ( coe1 ` ( i M j ) ) ` l ) = ( 0g ` R ) ) )
17	16	bicomd	\|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( A. l e. NN ( ( coe1 ` ( i M j ) ) ` l ) = ( 0g ` R ) <-> E. k e. K ( i M j ) = ( A ` k ) ) )
18	17	2ralbidva	\|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( A. i e. N A. j e. N A. l e. NN ( ( coe1 ` ( i M j ) ) ` l ) = ( 0g ` R ) <-> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
19	7 18	bitrd	\|- ( ( 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 ) ) )