This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ∅