Step |
Hyp |
Ref |
Expression |
1 |
|
matrcl.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
2 |
|
matrcl.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
3 |
|
n0i |
⊢ ( 𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅ ) |
4 |
|
df-mat |
⊢ Mat = ( 𝑎 ∈ Fin , 𝑏 ∈ V ↦ ( ( 𝑏 freeLMod ( 𝑎 × 𝑎 ) ) sSet 〈 ( .r ‘ ndx ) , ( 𝑏 maMul 〈 𝑎 , 𝑎 , 𝑎 〉 ) 〉 ) ) |
5 |
4
|
mpondm0 |
⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ∅ ) |
6 |
1 5
|
syl5eq |
⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐴 = ∅ ) |
7 |
6
|
fveq2d |
⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) ) |
8 |
|
base0 |
⊢ ∅ = ( Base ‘ ∅ ) |
9 |
7 2 8
|
3eqtr4g |
⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐵 = ∅ ) |
10 |
3 9
|
nsyl2 |
⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) ) |