Metamath Proof Explorer

Theorem matbas2d

Description: The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018)

Ref Expression
Hypotheses matbas2.a 
|- A = ( N Mat R )
matbas2.k 
|- K = ( Base ` R )
matbas2i.b 
|- B = ( Base ` A )
matbas2d.n 
|- ( ph -> N e. Fin )
matbas2d.r 
|- ( ph -> R e. V )
matbas2d.c 
|- ( ( ph /\ x e. N /\ y e. N ) -> C e. K )
Assertion matbas2d 
|- ( ph -> ( x e. N , y e. N |-> C ) e. B )

Proof

Step Hyp Ref Expression
1 matbas2.a 
 |-  A = ( N Mat R )
2 matbas2.k 
 |-  K = ( Base ` R )
3 matbas2i.b 
 |-  B = ( Base ` A )
4 matbas2d.n 
 |-  ( ph -> N e. Fin )
5 matbas2d.r 
 |-  ( ph -> R e. V )
6 matbas2d.c 
 |-  ( ( ph /\ x e. N /\ y e. N ) -> C e. K )
7 6 3expb 
 |-  ( ( ph /\ ( x e. N /\ y e. N ) ) -> C e. K )
8 7 ralrimivva 
 |-  ( ph -> A. x e. N A. y e. N C e. K )
9 eqid 
 |-  ( x e. N , y e. N |-> C ) = ( x e. N , y e. N |-> C )
10 9 fmpo 
 |-  ( A. x e. N A. y e. N C e. K <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K )
11 8 10 sylib 
 |-  ( ph -> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K )
12 1 2 matbas2 
 |-  ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
13 4 5 12 syl2anc 
 |-  ( ph -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
14 3 13 eqtr4id 
 |-  ( ph -> B = ( K ^m ( N X. N ) ) )
15 14 eleq2d 
 |-  ( ph -> ( ( x e. N , y e. N |-> C ) e. B <-> ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) ) )
16 2 fvexi 
 |-  K e. _V
17 4 4 xpexd 
 |-  ( ph -> ( N X. N ) e. _V )
18 elmapg 
 |-  ( ( K e. _V /\ ( N X. N ) e. _V ) -> ( ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) )
19 16 17 18 sylancr 
 |-  ( ph -> ( ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) )
20 15 19 bitrd 
 |-  ( ph -> ( ( x e. N , y e. N |-> C ) e. B <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) )
21 11 20 mpbird 
 |-  ( ph -> ( x e. N , y e. N |-> C ) e. B )