Step |
Hyp |
Ref |
Expression |
1 |
|
m2cpminv.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
2 |
|
m2cpminv.k |
⊢ 𝐾 = ( Base ‘ 𝐴 ) |
3 |
|
m2cpminv.s |
⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 ) |
4 |
|
m2cpminv.i |
⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 ) |
5 |
|
m2cpminv.t |
⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 ) |
6 |
1 2 3 4
|
cpm2mf |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆 ⟶ 𝐾 ) |
7 |
3 5 1 2
|
m2cpmf |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 ⟶ 𝑆 ) |
8 |
3 4 5
|
m2cpminvid2 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 ) |
9 |
8
|
3expa |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 ) |
10 |
9
|
ralrimiva |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑠 ∈ 𝑆 ( 𝑇 ‘ ( 𝐼 ‘ 𝑠 ) ) = 𝑠 ) |
11 |
4 1 2 5
|
m2cpminvid |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 ) |
12 |
11
|
3expa |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 ) |
13 |
12
|
ralrimiva |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑘 ∈ 𝐾 ( 𝐼 ‘ ( 𝑇 ‘ 𝑘 ) ) = 𝑘 ) |
14 |
6 7 10 13
|
2fvidf1od |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆 –1-1-onto→ 𝐾 ) |
15 |
6 7 10 13
|
2fvidinvd |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ◡ 𝐼 = 𝑇 ) |
16 |
14 15
|
jca |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 : 𝑆 –1-1-onto→ 𝐾 ∧ ◡ 𝐼 = 𝑇 ) ) |