| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢ (𝐼(subMat1‘ 1 )𝐼) = (𝐼(subMat1‘ 1 )𝐼) | 
| 2 |  | 1smat1.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑁 ∈ ℕ) | 
| 4 |  | 1smat1.i | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝐼 ∈ (1...𝑁)) | 
| 6 |  | 1smat1.r | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 7 |  | fzfi 14014 | . . . . . . . 8
⊢
(1...𝑁) ∈
Fin | 
| 8 |  | eqid 2736 | . . . . . . . . 9
⊢
((1...𝑁) Mat 𝑅) = ((1...𝑁) Mat 𝑅) | 
| 9 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘((1...𝑁)
Mat 𝑅)) =
(Base‘((1...𝑁) Mat
𝑅)) | 
| 10 |  | 1smat1.1 | . . . . . . . . 9
⊢  1 =
(1r‘((1...𝑁) Mat 𝑅)) | 
| 11 | 8, 9, 10 | mat1bas 22456 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (1...𝑁) ∈ Fin) → 1 ∈
(Base‘((1...𝑁) Mat
𝑅))) | 
| 12 | 6, 7, 11 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → 1 ∈
(Base‘((1...𝑁) Mat
𝑅))) | 
| 13 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 14 | 8, 13 | matbas2 22428 | . . . . . . . 8
⊢
(((1...𝑁) ∈ Fin
∧ 𝑅 ∈ Ring) →
((Base‘𝑅)
↑m ((1...𝑁)
× (1...𝑁))) =
(Base‘((1...𝑁) Mat
𝑅))) | 
| 15 | 7, 6, 14 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → ((Base‘𝑅) ↑m ((1...𝑁) × (1...𝑁))) = (Base‘((1...𝑁) Mat 𝑅))) | 
| 16 | 12, 15 | eleqtrrd 2843 | . . . . . 6
⊢ (𝜑 → 1 ∈ ((Base‘𝑅) ↑m ((1...𝑁) × (1...𝑁)))) | 
| 17 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 1 ∈ ((Base‘𝑅) ↑m ((1...𝑁) × (1...𝑁)))) | 
| 18 |  | fz1ssnn 13596 | . . . . . 6
⊢
(1...(𝑁 − 1))
⊆ ℕ | 
| 19 |  | simprl 770 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ (1...(𝑁 − 1))) | 
| 20 | 18, 19 | sselid 3980 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ ℕ) | 
| 21 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ (1...(𝑁 − 1))) | 
| 22 | 18, 21 | sselid 3980 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ ℕ) | 
| 23 |  | eqidd 2737 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑖 < 𝐼, 𝑖, (𝑖 + 1))) | 
| 24 |  | eqidd 2737 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1))) | 
| 25 | 1, 3, 3, 5, 5, 17,
20, 22, 23, 24 | smatlem 33797 | . . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝐼(subMat1‘ 1 )𝐼)𝑗) = (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) 1 if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)))) | 
| 26 |  | eqid 2736 | . . . . 5
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 27 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 28 | 7 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (1...𝑁) ∈ Fin) | 
| 29 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑅 ∈ Ring) | 
| 30 |  | nnuz 12922 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 31 | 20, 30 | eleqtrdi 2850 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈
(ℤ≥‘1)) | 
| 32 |  | fznatpl1 13619 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...(𝑁 − 1))) → (𝑖 + 1) ∈ (1...𝑁)) | 
| 33 | 3, 19, 32 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖 + 1) ∈ (1...𝑁)) | 
| 34 |  | peano2fzr 13578 | . . . . . . . 8
⊢ ((𝑖 ∈
(ℤ≥‘1) ∧ (𝑖 + 1) ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁)) | 
| 35 | 31, 33, 34 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ (1...𝑁)) | 
| 36 | 35, 33 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖 ∈ (1...𝑁) ∧ (𝑖 + 1) ∈ (1...𝑁))) | 
| 37 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑖 = if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) → (𝑖 ∈ (1...𝑁) ↔ if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) ∈ (1...𝑁))) | 
| 38 |  | eleq1 2828 | . . . . . . 7
⊢ ((𝑖 + 1) = if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) → ((𝑖 + 1) ∈ (1...𝑁) ↔ if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) ∈ (1...𝑁))) | 
| 39 | 37, 38 | ifboth 4564 | . . . . . 6
⊢ ((𝑖 ∈ (1...𝑁) ∧ (𝑖 + 1) ∈ (1...𝑁)) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) ∈ (1...𝑁)) | 
| 40 | 36, 39 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) ∈ (1...𝑁)) | 
| 41 | 22, 30 | eleqtrdi 2850 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈
(ℤ≥‘1)) | 
| 42 |  | fznatpl1 13619 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝑗 + 1) ∈ (1...𝑁)) | 
| 43 | 3, 21, 42 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑗 + 1) ∈ (1...𝑁)) | 
| 44 |  | peano2fzr 13578 | . . . . . . . 8
⊢ ((𝑗 ∈
(ℤ≥‘1) ∧ (𝑗 + 1) ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) | 
| 45 | 41, 43, 44 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ (1...𝑁)) | 
| 46 | 45, 43 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑗 ∈ (1...𝑁) ∧ (𝑗 + 1) ∈ (1...𝑁))) | 
| 47 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑗 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) → (𝑗 ∈ (1...𝑁) ↔ if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ∈ (1...𝑁))) | 
| 48 |  | eleq1 2828 | . . . . . . 7
⊢ ((𝑗 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) → ((𝑗 + 1) ∈ (1...𝑁) ↔ if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ∈ (1...𝑁))) | 
| 49 | 47, 48 | ifboth 4564 | . . . . . 6
⊢ ((𝑗 ∈ (1...𝑁) ∧ (𝑗 + 1) ∈ (1...𝑁)) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ∈ (1...𝑁)) | 
| 50 | 46, 49 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ∈ (1...𝑁)) | 
| 51 | 8, 26, 27, 28, 29, 40, 50, 10 | mat1ov 22455 | . . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) 1 if(𝑗 < 𝐼, 𝑗, (𝑗 + 1))) = if(if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)), (1r‘𝑅), (0g‘𝑅))) | 
| 52 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) → 𝑖 < 𝐼) | 
| 53 | 52 | iftrued 4532 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = 𝑖) | 
| 54 | 53 | eqeq1d 2738 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)))) | 
| 55 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼) | 
| 56 | 55 | iftrued 4532 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) = 𝑗) | 
| 57 | 56 | eqeq2d 2747 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → (𝑖 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 58 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ¬ 𝑗 < 𝐼) | 
| 59 | 58 | iffalsed 4535 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) = (𝑗 + 1)) | 
| 60 | 59 | eqeq2d 2747 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → (𝑖 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = (𝑗 + 1))) | 
| 61 | 20 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ ℝ) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 ∈ ℝ) | 
| 63 |  | fz1ssnn 13596 | . . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ⊆
ℕ | 
| 64 | 63, 4 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 65 | 64 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 66 | 65 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝐼 ∈ ℝ) | 
| 67 | 22 | nnred 12282 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ ℝ) | 
| 68 | 67 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑗 ∈ ℝ) | 
| 69 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 1 ∈ ℝ) | 
| 70 | 68, 69 | readdcld 11291 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → (𝑗 + 1) ∈ ℝ) | 
| 71 | 52 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 < 𝐼) | 
| 72 | 64 | nnzd 12642 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 73 | 72 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝐼 ∈ ℤ) | 
| 74 | 22 | nnzd 12642 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ ℤ) | 
| 75 | 74 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑗 ∈ ℤ) | 
| 76 | 66, 68, 58 | nltled 11412 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝐼 ≤ 𝑗) | 
| 77 |  | zleltp1 12670 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝐼 ≤ 𝑗 ↔ 𝐼 < (𝑗 + 1))) | 
| 78 | 77 | biimpa 476 | . . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ 𝐼 ≤ 𝑗) → 𝐼 < (𝑗 + 1)) | 
| 79 | 73, 75, 76, 78 | syl21anc 837 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝐼 < (𝑗 + 1)) | 
| 80 | 62, 66, 70, 71, 79 | lttrd 11423 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 < (𝑗 + 1)) | 
| 81 | 62, 80 | ltned 11398 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 ≠ (𝑗 + 1)) | 
| 82 | 81 | neneqd 2944 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ¬ 𝑖 = (𝑗 + 1)) | 
| 83 | 62, 66, 68, 71, 76 | ltletrd 11422 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 < 𝑗) | 
| 84 | 62, 83 | ltned 11398 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → 𝑖 ≠ 𝑗) | 
| 85 | 84 | neneqd 2944 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ¬ 𝑖 = 𝑗) | 
| 86 | 82, 85 | 2falsed 376 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → (𝑖 = (𝑗 + 1) ↔ 𝑖 = 𝑗)) | 
| 87 | 60, 86 | bitrd 279 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → (𝑖 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 88 | 57, 87 | pm2.61dan 812 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) → (𝑖 = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 89 | 54, 88 | bitrd 279 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ 𝑖 < 𝐼) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 90 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) → ¬ 𝑖 < 𝐼) | 
| 91 | 90 | iffalsed 4535 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = (𝑖 + 1)) | 
| 92 | 91 | eqeq1d 2738 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ (𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)))) | 
| 93 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼) | 
| 94 | 93 | iftrued 4532 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) = 𝑗) | 
| 95 | 94 | eqeq2d 2747 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ((𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ (𝑖 + 1) = 𝑗)) | 
| 96 | 67 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ) | 
| 97 | 65 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ) | 
| 98 | 61 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑖 ∈ ℝ) | 
| 99 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 1 ∈ ℝ) | 
| 100 | 98, 99 | readdcld 11291 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → (𝑖 + 1) ∈ ℝ) | 
| 101 | 72 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℤ) | 
| 102 | 20 | nnzd 12642 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ ℤ) | 
| 103 | 102 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑖 ∈ ℤ) | 
| 104 | 90 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ¬ 𝑖 < 𝐼) | 
| 105 | 97, 98, 104 | nltled 11412 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝐼 ≤ 𝑖) | 
| 106 |  | zleltp1 12670 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝐼 ≤ 𝑖 ↔ 𝐼 < (𝑖 + 1))) | 
| 107 | 106 | biimpa 476 | . . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝐼 ≤ 𝑖) → 𝐼 < (𝑖 + 1)) | 
| 108 | 101, 103,
105, 107 | syl21anc 837 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝐼 < (𝑖 + 1)) | 
| 109 | 96, 97, 100, 93, 108 | lttrd 11423 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 < (𝑖 + 1)) | 
| 110 | 96, 109 | ltned 11398 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 ≠ (𝑖 + 1)) | 
| 111 | 110 | necomd 2995 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → (𝑖 + 1) ≠ 𝑗) | 
| 112 | 111 | neneqd 2944 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ¬ (𝑖 + 1) = 𝑗) | 
| 113 | 96, 97, 98, 93, 105 | ltletrd 11422 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 < 𝑖) | 
| 114 | 96, 113 | ltned 11398 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑗 ≠ 𝑖) | 
| 115 | 114 | necomd 2995 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → 𝑖 ≠ 𝑗) | 
| 116 | 115 | neneqd 2944 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ¬ 𝑖 = 𝑗) | 
| 117 | 112, 116 | 2falsed 376 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ((𝑖 + 1) = 𝑗 ↔ 𝑖 = 𝑗)) | 
| 118 | 95, 117 | bitrd 279 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ 𝑗 < 𝐼) → ((𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 119 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ¬ 𝑗 < 𝐼) | 
| 120 | 119 | iffalsed 4535 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) = (𝑗 + 1)) | 
| 121 | 120 | eqeq2d 2747 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ((𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ (𝑖 + 1) = (𝑗 + 1))) | 
| 122 | 20 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ ℂ) | 
| 123 | 122 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ (𝑖 + 1) = (𝑗 + 1)) → 𝑖 ∈ ℂ) | 
| 124 | 22 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ ℂ) | 
| 125 | 124 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ (𝑖 + 1) = (𝑗 + 1)) → 𝑗 ∈ ℂ) | 
| 126 |  | 1cnd 11257 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ (𝑖 + 1) = (𝑗 + 1)) → 1 ∈
ℂ) | 
| 127 |  | simpr 484 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ (𝑖 + 1) = (𝑗 + 1)) → (𝑖 + 1) = (𝑗 + 1)) | 
| 128 | 123, 125,
126, 127 | addcan2ad 11468 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ (𝑖 + 1) = (𝑗 + 1)) → 𝑖 = 𝑗) | 
| 129 |  | simpr 484 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗) | 
| 130 | 129 | oveq1d 7447 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) ∧ 𝑖 = 𝑗) → (𝑖 + 1) = (𝑗 + 1)) | 
| 131 | 128, 130 | impbida 800 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ((𝑖 + 1) = (𝑗 + 1) ↔ 𝑖 = 𝑗)) | 
| 132 | 121, 131 | bitrd 279 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) ∧ ¬ 𝑗 < 𝐼) → ((𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 133 | 118, 132 | pm2.61dan 812 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) → ((𝑖 + 1) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 134 | 92, 133 | bitrd 279 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) ∧ ¬ 𝑖 < 𝐼) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 135 | 89, 134 | pm2.61dan 812 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)) ↔ 𝑖 = 𝑗)) | 
| 136 | 135 | ifbid 4548 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)), (1r‘𝑅), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) | 
| 137 |  | eqid 2736 | . . . . . 6
⊢
((1...(𝑁 − 1))
Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅) | 
| 138 |  | fzfid 14015 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (1...(𝑁 − 1)) ∈
Fin) | 
| 139 |  | eqid 2736 | . . . . . 6
⊢
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)) | 
| 140 | 137, 26, 27, 138, 29, 19, 21, 139 | mat1ov 22455 | . . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) | 
| 141 | 136, 140 | eqtr4d 2779 | . . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑗 < 𝐼, 𝑗, (𝑗 + 1)), (1r‘𝑅), (0g‘𝑅)) = (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗)) | 
| 142 | 25, 51, 141 | 3eqtrd 2780 | . . 3
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝐼(subMat1‘ 1 )𝐼)𝑗) = (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗)) | 
| 143 | 142 | ralrimivva 3201 | . 2
⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘ 1 )𝐼)𝑗) = (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗)) | 
| 144 | 1, 2, 2, 4, 4, 16 | smatrcl 33796 | . . . 4
⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) ∈ ((Base‘𝑅) ↑m ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) | 
| 145 |  | elmapfn 8906 | . . . 4
⊢ ((𝐼(subMat1‘ 1 )𝐼) ∈ ((Base‘𝑅) ↑m
((1...(𝑁 − 1))
× (1...(𝑁 −
1)))) → (𝐼(subMat1‘ 1 )𝐼) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) | 
| 146 | 144, 145 | syl 17 | . . 3
⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) | 
| 147 |  | fzfi 14014 | . . . . . 6
⊢
(1...(𝑁 − 1))
∈ Fin | 
| 148 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) | 
| 149 | 137, 148,
139 | mat1bas 22456 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (1...(𝑁 − 1)) ∈ Fin) →
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 150 | 6, 147, 149 | sylancl 586 | . . . . 5
⊢ (𝜑 →
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 151 | 137, 13 | matbas2 22428 | . . . . . 6
⊢
(((1...(𝑁 −
1)) ∈ Fin ∧ 𝑅
∈ Ring) → ((Base‘𝑅) ↑m ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅))) | 
| 152 | 147, 6, 151 | sylancr 587 | . . . . 5
⊢ (𝜑 → ((Base‘𝑅) ↑m
((1...(𝑁 − 1))
× (1...(𝑁 −
1)))) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 153 | 150, 152 | eleqtrrd 2843 | . . . 4
⊢ (𝜑 →
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) ∈ ((Base‘𝑅) ↑m ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) | 
| 154 |  | elmapfn 8906 | . . . 4
⊢
((1r‘((1...(𝑁 − 1)) Mat 𝑅)) ∈ ((Base‘𝑅) ↑m ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) →
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) | 
| 155 | 153, 154 | syl 17 | . . 3
⊢ (𝜑 →
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) | 
| 156 |  | eqfnov2 7564 | . . 3
⊢ (((𝐼(subMat1‘ 1 )𝐼) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1))) ∧
(1r‘((1...(𝑁 − 1)) Mat 𝑅)) Fn ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) → ((𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)) ↔ ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘ 1 )𝐼)𝑗) = (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗))) | 
| 157 | 146, 155,
156 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)) ↔ ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘ 1 )𝐼)𝑗) = (𝑖(1r‘((1...(𝑁 − 1)) Mat 𝑅))𝑗))) | 
| 158 | 143, 157 | mpbird 257 | 1
⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅))) |