Metamath Proof Explorer


Theorem matbas

Description: The matrix ring has the same base set as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
matbas.g 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
Assertion matbas ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 matbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 matbas.g 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3 baseid Base = Slot ( Base ‘ ndx )
4 basendxnmulrndx ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
5 3 4 setsnid ( Base ‘ 𝐺 ) = ( Base ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
6 eqid ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
7 1 2 6 matval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
8 7 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) ) )
9 5 8 eqtr4id ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐴 ) )