Step |
Hyp |
Ref |
Expression |
1 |
|
matval.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
2 |
|
matval.g |
⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) |
3 |
|
matval.t |
⊢ · = ( 𝑅 maMul 〈 𝑁 , 𝑁 , 𝑁 〉 ) |
4 |
|
elex |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V ) |
5 |
|
id |
⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 ) |
6 |
|
id |
⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 ) |
7 |
6
|
sqxpeqd |
⊢ ( 𝑛 = 𝑁 → ( 𝑛 × 𝑛 ) = ( 𝑁 × 𝑁 ) ) |
8 |
5 7
|
oveqan12rd |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) |
9 |
8 2
|
eqtr4di |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) = 𝐺 ) |
10 |
6 6 6
|
oteq123d |
⊢ ( 𝑛 = 𝑁 → 〈 𝑛 , 𝑛 , 𝑛 〉 = 〈 𝑁 , 𝑁 , 𝑁 〉 ) |
11 |
5 10
|
oveqan12rd |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 maMul 〈 𝑛 , 𝑛 , 𝑛 〉 ) = ( 𝑅 maMul 〈 𝑁 , 𝑁 , 𝑁 〉 ) ) |
12 |
11 3
|
eqtr4di |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 maMul 〈 𝑛 , 𝑛 , 𝑛 〉 ) = · ) |
13 |
12
|
opeq2d |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 〈 ( .r ‘ ndx ) , ( 𝑟 maMul 〈 𝑛 , 𝑛 , 𝑛 〉 ) 〉 = 〈 ( .r ‘ ndx ) , · 〉 ) |
14 |
9 13
|
oveq12d |
⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet 〈 ( .r ‘ ndx ) , ( 𝑟 maMul 〈 𝑛 , 𝑛 , 𝑛 〉 ) 〉 ) = ( 𝐺 sSet 〈 ( .r ‘ ndx ) , · 〉 ) ) |
15 |
|
df-mat |
⊢ Mat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet 〈 ( .r ‘ ndx ) , ( 𝑟 maMul 〈 𝑛 , 𝑛 , 𝑛 〉 ) 〉 ) ) |
16 |
|
ovex |
⊢ ( 𝐺 sSet 〈 ( .r ‘ ndx ) , · 〉 ) ∈ V |
17 |
14 15 16
|
ovmpoa |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ( 𝐺 sSet 〈 ( .r ‘ ndx ) , · 〉 ) ) |
18 |
4 17
|
sylan2 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 Mat 𝑅 ) = ( 𝐺 sSet 〈 ( .r ‘ ndx ) , · 〉 ) ) |
19 |
1 18
|
syl5eq |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet 〈 ( .r ‘ ndx ) , · 〉 ) ) |