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 |
|
df-cpmat |
|- ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } ) |
6 |
5
|
a1i |
|- ( ( N e. Fin /\ R e. V ) -> ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } ) ) |
7 |
|
simpl |
|- ( ( n = N /\ r = R ) -> n = N ) |
8 |
|
fveq2 |
|- ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) ) |
9 |
8
|
adantl |
|- ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = ( Poly1 ` R ) ) |
10 |
7 9
|
oveq12d |
|- ( ( n = N /\ r = R ) -> ( n Mat ( Poly1 ` r ) ) = ( N Mat ( Poly1 ` R ) ) ) |
11 |
10
|
fveq2d |
|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) |
12 |
2
|
oveq2i |
|- ( N Mat P ) = ( N Mat ( Poly1 ` R ) ) |
13 |
3 12
|
eqtri |
|- C = ( N Mat ( Poly1 ` R ) ) |
14 |
13
|
fveq2i |
|- ( Base ` C ) = ( Base ` ( N Mat ( Poly1 ` R ) ) ) |
15 |
4 14
|
eqtri |
|- B = ( Base ` ( N Mat ( Poly1 ` R ) ) ) |
16 |
11 15
|
eqtr4di |
|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = B ) |
17 |
|
fveq2 |
|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) ) |
18 |
17
|
adantl |
|- ( ( n = N /\ r = R ) -> ( 0g ` r ) = ( 0g ` R ) ) |
19 |
18
|
eqeq2d |
|- ( ( n = N /\ r = R ) -> ( ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) ) |
20 |
19
|
ralbidv |
|- ( ( n = N /\ r = R ) -> ( A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) ) |
21 |
7 20
|
raleqbidv |
|- ( ( n = N /\ r = R ) -> ( A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) ) |
22 |
7 21
|
raleqbidv |
|- ( ( n = N /\ r = R ) -> ( A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) ) |
23 |
16 22
|
rabeqbidv |
|- ( ( n = N /\ r = R ) -> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } ) |
24 |
23
|
adantl |
|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } ) |
25 |
|
simpl |
|- ( ( N e. Fin /\ R e. V ) -> N e. Fin ) |
26 |
|
elex |
|- ( R e. V -> R e. _V ) |
27 |
26
|
adantl |
|- ( ( N e. Fin /\ R e. V ) -> R e. _V ) |
28 |
4
|
fvexi |
|- B e. _V |
29 |
|
rabexg |
|- ( B e. _V -> { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } e. _V ) |
30 |
28 29
|
mp1i |
|- ( ( N e. Fin /\ R e. V ) -> { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } e. _V ) |
31 |
6 24 25 27 30
|
ovmpod |
|- ( ( N e. Fin /\ R e. V ) -> ( N ConstPolyMat R ) = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } ) |
32 |
1 31
|
syl5eq |
|- ( ( N e. Fin /\ R e. V ) -> S = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } ) |