Proof of Theorem madjusmdetlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | madjusmdet.m | . . . 4
⊢ (𝜑 → 𝑀 ∈ 𝐵) | 
| 2 |  | madjusmdet.j | . . . 4
⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) | 
| 3 |  | madjusmdet.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) | 
| 4 |  | madjusmdet.a | . . . . 5
⊢ 𝐴 = ((1...𝑁) Mat 𝑅) | 
| 5 |  | madjusmdet.b | . . . . 5
⊢ 𝐵 = (Base‘𝐴) | 
| 6 |  | madjusmdet.d | . . . . 5
⊢ 𝐷 = ((1...𝑁) maDet 𝑅) | 
| 7 |  | madjusmdet.k | . . . . 5
⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) | 
| 8 | 4, 5, 6, 7 | maducoevalmin1 22659 | . . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))) | 
| 9 | 1, 2, 3, 8 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))) | 
| 10 |  | madjusmdetlem1.u | . . . 4
⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) | 
| 11 | 10 | fveq2i 6908 | . . 3
⊢ (𝐷‘𝑈) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)) | 
| 12 | 9, 11 | eqtr4di 2794 | . 2
⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘𝑈)) | 
| 13 |  | madjusmdetlem1.g | . . 3
⊢ 𝐺 =
(Base‘(SymGrp‘(1...𝑁))) | 
| 14 |  | madjusmdetlem1.s | . . 3
⊢ 𝑆 = (pmSgn‘(1...𝑁)) | 
| 15 |  | madjusmdet.z | . . 3
⊢ 𝑍 = (ℤRHom‘𝑅) | 
| 16 |  | madjusmdet.t | . . 3
⊢  · =
(.r‘𝑅) | 
| 17 |  | madjusmdetlem1.w | . . 3
⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) | 
| 18 |  | madjusmdet.r | . . 3
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 19 |  | fzfid 14015 | . . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) | 
| 20 |  | crngring 20243 | . . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 21 | 18, 20 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 22 | 4, 5 | minmar1cl 22658 | . . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵) | 
| 23 | 21, 1, 3, 2, 22 | syl22anc 838 | . . . 4
⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵) | 
| 24 | 10, 23 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝑈 ∈ 𝐵) | 
| 25 |  | madjusmdetlem1.p | . . 3
⊢ (𝜑 → 𝑃 ∈ 𝐺) | 
| 26 |  | madjusmdetlem1.q | . . 3
⊢ (𝜑 → 𝑄 ∈ 𝐺) | 
| 27 | 4, 5, 6, 13, 14, 15, 16, 17, 18, 19, 24, 25, 26 | mdetpmtr12 33825 | . 2
⊢ (𝜑 → (𝐷‘𝑈) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊))) | 
| 28 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁) | 
| 29 | 28 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁)) | 
| 30 |  | madjusmdetlem1.1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃‘𝑁) = 𝐼) | 
| 31 | 30 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑁) = 𝐼) | 
| 32 | 31 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼) | 
| 33 | 29, 32 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼) | 
| 34 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑗 = 𝑁) | 
| 35 | 34 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = (𝑄‘𝑁)) | 
| 36 |  | madjusmdetlem1.2 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄‘𝑁) = 𝐽) | 
| 37 | 36 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑁) = 𝐽) | 
| 38 | 37 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑁) = 𝐽) | 
| 39 | 35, 38 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = 𝐽) | 
| 40 | 33, 39 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽)) | 
| 41 | 1 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑀 ∈ 𝐵) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵) | 
| 43 | 3 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁)) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁)) | 
| 45 | 2 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐽 ∈ (1...𝑁)) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁)) | 
| 47 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
((1...𝑁) minMatR1
𝑅) = ((1...𝑁) minMatR1 𝑅) | 
| 48 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 49 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 50 | 4, 5, 47, 48, 49 | minmar1eval 22656 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽))) | 
| 51 | 42, 44, 46, 44, 46, 50 | syl122anc 1380 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽))) | 
| 52 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ 𝐼 = 𝐼 | 
| 53 | 52 | iftruei 4531 | . . . . . . . . . . . . 13
⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) | 
| 54 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ 𝐽 = 𝐽 | 
| 55 | 54 | iftruei 4531 | . . . . . . . . . . . . 13
⊢ if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅) | 
| 56 | 53, 55 | eqtri 2764 | . . . . . . . . . . . 12
⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅) | 
| 57 | 56 | a1i 11 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅)) | 
| 58 | 40, 51, 57 | 3eqtrrd 2781 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (1r‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 59 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑖 = 𝑁) | 
| 60 | 59 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁)) | 
| 61 | 31 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼) | 
| 62 | 60, 61 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼) | 
| 63 | 62 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 64 | 41 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵) | 
| 65 | 43 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁)) | 
| 66 | 45 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁)) | 
| 67 | 26 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄 ∈ 𝐺) | 
| 68 |  | simp3 1138 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) | 
| 69 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁)) | 
| 70 | 69, 13 | symgfv 19398 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ 𝐺 ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁)) | 
| 71 | 67, 68, 70 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁)) | 
| 72 | 71 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑄‘𝑗) ∈ (1...𝑁)) | 
| 73 | 4, 5, 47, 48, 49 | minmar1eval 22656 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ (𝑄‘𝑗) ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗)))) | 
| 74 | 64, 65, 66, 65, 72, 73 | syl122anc 1380 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗)))) | 
| 75 | 52 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 = 𝐼) | 
| 76 | 75 | iftrued 4532 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅))) | 
| 77 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (𝑄‘𝑗) = 𝐽) | 
| 78 | 77 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = (◡𝑄‘𝐽)) | 
| 79 | 69, 13 | symgbasf1o 19393 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ 𝐺 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 80 | 67, 79 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 81 | 80 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 82 | 68 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 ∈ (1...𝑁)) | 
| 83 |  | f1ocnvfv1 7297 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗) | 
| 84 | 81, 82, 83 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗) | 
| 85 | 36 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = (◡𝑄‘𝐽)) | 
| 86 | 26, 79 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 87 |  | madjusmdet.n | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 88 |  | nnuz 12922 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) | 
| 89 | 87, 88 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) | 
| 90 |  | eluzfz2 13573 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) | 
| 91 | 89, 90 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) | 
| 92 |  | f1ocnvfv1 7297 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑁)) = 𝑁) | 
| 93 | 86, 91, 92 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = 𝑁) | 
| 94 | 85, 93 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡𝑄‘𝐽) = 𝑁) | 
| 95 | 94 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘𝐽) = 𝑁) | 
| 96 | 95 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘𝐽) = 𝑁) | 
| 97 | 78, 84, 96 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 = 𝑁) | 
| 98 | 97 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → ((𝑄‘𝑗) = 𝐽 → 𝑗 = 𝑁)) | 
| 99 | 98 | con3d 152 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → (¬ 𝑗 = 𝑁 → ¬ (𝑄‘𝑗) = 𝐽)) | 
| 100 | 99 | imp 406 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ¬ (𝑄‘𝑗) = 𝐽) | 
| 101 | 100 | iffalsed 4535 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) | 
| 102 | 76, 101 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = (0g‘𝑅)) | 
| 103 | 63, 74, 102 | 3eqtrrd 2781 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (0g‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 104 | 58, 103 | ifeqda 4561 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 105 |  | simp2 1137 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁)) | 
| 106 | 105 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑖 ∈ (1...𝑁)) | 
| 107 | 68 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑗 ∈ (1...𝑁)) | 
| 108 |  | ovexd 7467 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) | 
| 109 | 10 | oveqi 7445 | . . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) | 
| 110 | 109 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 111 | 110 | mpoeq3ia 7512 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 112 | 17, 111 | eqtri 2764 | . . . . . . . . . . 11
⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 113 | 112 | ovmpt4g 7581 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 114 | 106, 107,
108, 113 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 115 | 104, 114 | ifeqda 4561 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) | 
| 116 | 115 | mpoeq3dva 7511 | . . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))) | 
| 117 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 118 | 25 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑃 ∈ 𝐺) | 
| 119 | 69, 13 | symgfv 19398 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁)) | 
| 120 | 118, 105,
119 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁)) | 
| 121 | 24 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈 ∈ 𝐵) | 
| 122 | 4, 117, 5, 120, 71, 121 | matecld 22433 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) ∈ (Base‘𝑅)) | 
| 123 | 4, 117, 5, 19, 18, 122 | matbas2d 22430 | . . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) ∈ 𝐵) | 
| 124 | 17, 123 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ 𝐵) | 
| 125 | 117, 48 | ringidcl 20263 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 126 | 21, 125 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 127 |  | eqid 2736 | . . . . . . . . 9
⊢
((1...𝑁) matRRep
𝑅) = ((1...𝑁) matRRep 𝑅) | 
| 128 | 4, 5, 127, 49 | marrepval 22569 | . . . . . . . 8
⊢ (((𝑊 ∈ 𝐵 ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ (𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)))) | 
| 129 | 124, 126,
91, 91, 128 | syl22anc 838 | . . . . . . 7
⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)))) | 
| 130 | 112 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))) | 
| 131 | 116, 129,
130 | 3eqtr4d 2786 | . . . . . 6
⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = 𝑊) | 
| 132 | 131 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐷‘𝑊)) | 
| 133 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
((1...𝑁) subMat
𝑅) = ((1...𝑁) subMat 𝑅) | 
| 134 | 4, 133, 5 | submaval 22588 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗))) | 
| 135 | 124, 91, 91, 134 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗))) | 
| 136 |  | fzdif2 32793 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) | 
| 137 | 89, 136 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) | 
| 138 |  | mpoeq12 7507 | . . . . . . . . . . 11
⊢
((((1...𝑁) ∖
{𝑁}) = (1...(𝑁 − 1)) ∧ ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) | 
| 139 | 137, 137,
138 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) | 
| 140 | 135, 139 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) | 
| 141 |  | difssd 4136 | . . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁)) | 
| 142 | 137, 141 | eqsstrrd 4018 | . . . . . . . . . 10
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) | 
| 143 | 4, 5 | submabas 22585 | . . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐵 ∧ (1...(𝑁 − 1)) ⊆ (1...𝑁)) → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 144 | 124, 142,
143 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 145 | 140, 144 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) | 
| 146 |  | madjusmdet.e | . . . . . . . . 9
⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) | 
| 147 |  | eqid 2736 | . . . . . . . . 9
⊢
((1...(𝑁 − 1))
Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅) | 
| 148 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) | 
| 149 | 146, 147,
148, 117 | mdetcl 22603 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) | 
| 150 | 18, 145, 149 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) | 
| 151 | 117, 16, 48 | ringlidm 20267 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) | 
| 152 | 21, 150, 151 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
((1r‘𝑅)
·
(𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) | 
| 153 | 4 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(Base‘𝐴) =
(Base‘((1...𝑁) Mat
𝑅)) | 
| 154 | 5, 153 | eqtri 2764 | . . . . . . . . . 10
⊢ 𝐵 = (Base‘((1...𝑁) Mat 𝑅)) | 
| 155 | 124, 154 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) | 
| 156 |  | smadiadetr 22682 | . . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) ∧ (𝑁 ∈ (1...𝑁) ∧ (1r‘𝑅) ∈ (Base‘𝑅))) → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 157 | 18, 155, 91, 126, 156 | syl22anc 838 | . . . . . . . 8
⊢ (𝜑 → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 158 | 6 | fveq1i 6906 | . . . . . . . . 9
⊢ (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) | 
| 159 | 16 | oveqi 7445 | . . . . . . . . 9
⊢
((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) | 
| 160 | 158, 159 | eqeq12i 2754 | . . . . . . . 8
⊢ ((𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) ↔ (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 161 | 157, 160 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 162 | 137 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅)) | 
| 163 | 162, 146 | eqtr4di 2794 | . . . . . . . . 9
⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸) | 
| 164 | 163 | fveq1d 6907 | . . . . . . . 8
⊢ (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) | 
| 165 | 164 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 →
((1r‘𝑅)
·
((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 166 | 161, 165 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) | 
| 167 | 4, 5 | submat1n 33805 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) | 
| 168 | 87, 124, 167 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) | 
| 169 | 168 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → (𝐸‘(𝑁(subMat1‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) | 
| 170 | 152, 166,
169 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) | 
| 171 | 132, 170 | eqtr3d 2778 | . . . 4
⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) | 
| 172 | 4, 5, 87, 3, 2, 21, 1, 10 | submatminr1 33810 | . . . . . 6
⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽)) | 
| 173 |  | madjusmdetlem1.3 | . . . . . 6
⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) | 
| 174 | 172, 173 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) | 
| 175 | 174 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) | 
| 176 | 171, 175 | eqtr4d 2779 | . . 3
⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) | 
| 177 | 176 | oveq2d 7448 | . 2
⊢ (𝜑 → ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | 
| 178 | 12, 27, 177 | 3eqtrd 2780 | 1
⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) |