![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > matbas2i | Structured version Visualization version Unicode version |
Description: A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
Ref | Expression |
---|---|
matbas2.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
matbas2.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
matbas2i.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
matbas2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | matbas2i.b |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6eleq 2539 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | matbas2.a |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4, 2 | matrcl 19447 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | matbas2.k |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 6 | matbas2 19456 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | eleqtrrd 2532 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |