MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  matbas2d Structured version   Unicode version

Theorem matbas2d 19033
Description: The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018.)
Hypotheses
Ref Expression
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
Ref Expression
matbas2d  |-  ( ph  ->  ( x  e.  N ,  y  e.  N  |->  C )  e.  B
)
Distinct variable groups:    ph, x, y   
x, N, y    x, K, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    R( x, y)    V( x, y)

Proof of Theorem matbas2d
StepHypRef Expression
1 matbas2d.c . . . . 5  |-  ( (
ph  /\  x  e.  N  /\  y  e.  N
)  ->  C  e.  K )
213expb 1195 . . . 4  |-  ( (
ph  /\  ( x  e.  N  /\  y  e.  N ) )  ->  C  e.  K )
32ralrimivva 2817 . . 3  |-  ( ph  ->  A. x  e.  N  A. y  e.  N  C  e.  K )
4 eqid 2396 . . . 4  |-  ( x  e.  N ,  y  e.  N  |->  C )  =  ( x  e.  N ,  y  e.  N  |->  C )
54fmpt2 6788 . . 3  |-  ( A. x  e.  N  A. y  e.  N  C  e.  K  <->  ( x  e.  N ,  y  e.  N  |->  C ) : ( N  X.  N
) --> K )
63, 5sylib 196 . 2  |-  ( ph  ->  ( x  e.  N ,  y  e.  N  |->  C ) : ( N  X.  N ) --> K )
7 matbas2d.n . . . . . 6  |-  ( ph  ->  N  e.  Fin )
8 matbas2d.r . . . . . 6  |-  ( ph  ->  R  e.  V )
9 matbas2.a . . . . . . 7  |-  A  =  ( N Mat  R )
10 matbas2.k . . . . . . 7  |-  K  =  ( Base `  R
)
119, 10matbas2 19031 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  V )  ->  ( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
127, 8, 11syl2anc 659 . . . . 5  |-  ( ph  ->  ( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
13 matbas2i.b . . . . 5  |-  B  =  ( Base `  A
)
1412, 13syl6reqr 2456 . . . 4  |-  ( ph  ->  B  =  ( K  ^m  ( N  X.  N ) ) )
1514eleq2d 2466 . . 3  |-  ( ph  ->  ( ( x  e.  N ,  y  e.  N  |->  C )  e.  B  <->  ( x  e.  N ,  y  e.  N  |->  C )  e.  ( K  ^m  ( N  X.  N ) ) ) )
16 fvex 5801 . . . . 5  |-  ( Base `  R )  e.  _V
1710, 16eqeltri 2480 . . . 4  |-  K  e. 
_V
18 xpexg 6523 . . . . 5  |-  ( ( N  e.  Fin  /\  N  e.  Fin )  ->  ( N  X.  N
)  e.  _V )
197, 7, 18syl2anc 659 . . . 4  |-  ( ph  ->  ( N  X.  N
)  e.  _V )
20 elmapg 7373 . . . 4  |-  ( ( 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 ) )
2117, 19, 20sylancr 661 . . 3  |-  ( 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 ) )
2215, 21bitrd 253 . 2  |-  ( ph  ->  ( ( x  e.  N ,  y  e.  N  |->  C )  e.  B  <->  ( x  e.  N ,  y  e.  N  |->  C ) : ( N  X.  N
) --> K ) )
236, 22mpbird 232 1  |-  ( ph  ->  ( x  e.  N ,  y  e.  N  |->  C )  e.  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 971    = wceq 1399    e. wcel 1836   A.wral 2746   _Vcvv 3051    X. cxp 4928   -->wf 5509   ` cfv 5513  (class class class)co 6218    |-> cmpt2 6220    ^m cmap 7360   Fincfn 7457   Basecbs 14657   Mat cmat 19017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-ot 3970  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-supp 6840  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-map 7362  df-ixp 7411  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-fsupp 7767  df-sup 7838  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-2 10533  df-3 10534  df-4 10535  df-5 10536  df-6 10537  df-7 10538  df-8 10539  df-9 10540  df-10 10541  df-n0 10735  df-z 10804  df-dec 10918  df-uz 11024  df-fz 11616  df-struct 14659  df-ndx 14660  df-slot 14661  df-base 14662  df-sets 14663  df-ress 14664  df-plusg 14738  df-mulr 14739  df-sca 14741  df-vsca 14742  df-ip 14743  df-tset 14744  df-ple 14745  df-ds 14747  df-hom 14749  df-cco 14750  df-0g 14872  df-prds 14878  df-pws 14880  df-sra 17954  df-rgmod 17955  df-dsmm 18877  df-frlm 18892  df-mat 19018
This theorem is referenced by:  mpt2matmul  19056  dmatmulcl  19110  scmatscmiddistr  19118  marrepcl  19174  marepvcl  19179  submabas  19188  mdetrsca2  19214  mdetr0  19215  mdetrlin2  19217  mdetralt2  19219  mdetero  19220  mdetunilem2  19223  mdetunilem5  19226  mdetunilem6  19227  maduf  19251  madutpos  19252  marep01ma  19270  mat2pmatbas  19335  mat2pmatghm  19339  cpm2mf  19361  m2cpminvid  19362  m2cpminvid2  19364  m2cpmfo  19365  decpmatcl  19376  decpmatmul  19381  pmatcollpw1  19385  pmatcollpw2  19387  monmatcollpw  19388  pmatcollpwlem  19389  pmatcollpw  19390  pmatcollpw3lem  19392  pmatcollpwscmatlem2  19399  pm2mpf1  19408  mply1topmatcl  19414  mp2pm2mplem2  19416  mp2pm2mplem4  19418  pm2mpghm  19425
  Copyright terms: Public domain W3C validator