Theorem matbas2i 19457

Description: A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.)

Hypotheses

Ref	Expression
matbas2.a	|- A = ( N Mat R )
matbas2.k	|- K = ( Base ` R )
matbas2i.b	|- B = ( Base ` A )

Assertion

Ref	Expression
matbas2i	|- ( M e. B -> M e. ( K ^m ( N X. N ) ) )

Proof of Theorem matbas2i

Step	Hyp	Ref	Expression
1		id 22	. . 3 |- ( M e. B -> M e. B )
2		matbas2i.b	. . 3 |- B = ( Base ` A )
3	1, 2	syl6eleq 2539	. 2 |- ( M e. B -> M e. ( Base ` A ) )
4		matbas2.a	. . . 4 |- A = ( N Mat R )
5	4, 2	matrcl 19447	. . 3 |- ( M e. B -> ( N e. Fin /\ R e. _V ) )
6		matbas2.k	. . . 4 |- K = ( Base ` R )
7	4, 6	matbas2 19456	. . 3 |- ( ( N e. Fin /\ R e. _V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
8	5, 7	syl 17	. 2 |- ( M e. B -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
9	3, 8	eleqtrrd 2532	1 |- ( M e. B -> M e. ( K ^m ( N X. N ) ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1447   e. wcel 1890   _Vcvv 3012   X. cxp 4809   ` cfv 5560  (class class class)co 6275   ^m cmap 7458   Fincfn 7555   Basecbs 15131   Mat cmat 19442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-ot 3944  df-uni 4168  df-int 4204  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-1st 6780  df-2nd 6781  df-supp 6902  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-1o 7168  df-oadd 7172  df-er 7349  df-map 7460  df-ixp 7509  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-fsupp 7870  df-sup 7942  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-5 10659  df-6 10660  df-7 10661  df-8 10662  df-9 10663  df-10 10664  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-fz 11775  df-struct 15133  df-ndx 15134  df-slot 15135  df-base 15136  df-sets 15137  df-ress 15138  df-plusg 15213  df-mulr 15214  df-sca 15216  df-vsca 15217  df-ip 15218  df-tset 15219  df-ple 15220  df-ds 15222  df-hom 15224  df-cco 15225  df-0g 15350  df-prds 15356  df-pws 15358  df-sra 18405  df-rgmod 18406  df-dsmm 19305  df-frlm 19320  df-mat 19443

This theorem is referenced by:  eqmat  19459  matplusgcell  19468  matsubgcell  19469  matmulcell  19480  mattposcl  19488  mattpostpos  19489  mattposm  19494  matgsumcl  19495  dmatmul  19532  mdetleib2  19623  mdetf  19630  mdetdiaglem  19633  mdetrlin  19637  mdetrsca  19638  mdetralt  19643  mdetunilem7  19653  mdetunilem9  19655  mdetmul  19658  maducoeval2  19675  madutpos  19677  madugsum  19678  madurid  19679  decpmatval  19799  decpmatmul  19806  pmatcollpw3lem  19817  smatcl  28634  matmpt2  28635  submat1n  28637  submateq  28641  madjusmdetlem3  28661