Metamath Proof Explorer


Theorem matbas0

Description: There is no matrix for a not finite dimension or a proper class as the underlying ring. (Contributed by AV, 28-Dec-2018)

Ref Expression
Assertion matbas0 ¬ N Fin R V Base N Mat R =

Proof

Step Hyp Ref Expression
1 df-mat Mat = n Fin , r V r freeLMod n × n sSet ndx r maMul n n n
2 1 mpondm0 ¬ N Fin R V N Mat R =
3 2 fveq2d ¬ N Fin R V Base N Mat R = Base
4 base0 = Base
5 3 4 eqtr4di ¬ N Fin R V Base N Mat R =