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 20277 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))) |
9 | 1, 2, 3, 8 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))) |
10 | | madjusmdetlem1.u |
. . . 4
⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) |
11 | 10 | fveq2i 6106 |
. . 3
⊢ (𝐷‘𝑈) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)) |
12 | 9, 11 | syl6eqr 2662 |
. 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 12634 |
. . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
20 | | crngring 18381 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
21 | 18, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
22 | 4, 5 | minmar1cl 20276 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵) |
23 | 21, 1, 3, 2, 22 | syl22anc 1319 |
. . . 4
⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵) |
24 | 10, 23 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
25 | | madjusmdetlem1.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐺) |
26 | | madjusmdetlem1.q |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐺) |
27 | 4, 5, 6, 13, 14, 15, 16, 17, 18, 19, 24, 25, 26 | mdetpmtr12 29219 |
. 2
⊢ (𝜑 → (𝐷‘𝑈) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊))) |
28 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁)) |
30 | | madjusmdetlem1.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃‘𝑁) = 𝐼) |
31 | 30 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑁) = 𝐼) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼) |
33 | 29, 32 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼) |
34 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑗 = 𝑁) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = (𝑄‘𝑁)) |
36 | | madjusmdetlem1.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄‘𝑁) = 𝐽) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑁) = 𝐽) |
38 | 37 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑁) = 𝐽) |
39 | 35, 38 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = 𝐽) |
40 | 33, 39 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽)) |
41 | 1 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑀 ∈ 𝐵) |
42 | 41 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵) |
43 | 3 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁)) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁)) |
45 | 2 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐽 ∈ (1...𝑁)) |
46 | 45 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁)) |
47 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((1...𝑁) minMatR1
𝑅) = ((1...𝑁) minMatR1 𝑅) |
48 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑅) = (1r‘𝑅) |
49 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
50 | 4, 5, 47, 48, 49 | minmar1eval 20274 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽))) |
51 | 42, 44, 46, 44, 46, 50 | syl122anc 1327 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽))) |
52 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ 𝐼 = 𝐼 |
53 | 52 | iftruei 4043 |
. . . . . . . . . . . . 13
⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) |
54 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ 𝐽 = 𝐽 |
55 | 54 | iftruei 4043 |
. . . . . . . . . . . . 13
⊢ if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅) |
56 | 53, 55 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅) |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅)) |
58 | 40, 51, 57 | 3eqtrrd 2649 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (1r‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
59 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑖 = 𝑁) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁)) |
61 | 31 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼) |
62 | 60, 61 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼) |
63 | 62 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
64 | 41 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵) |
65 | 43 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁)) |
66 | 45 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁)) |
67 | 26 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄 ∈ 𝐺) |
68 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) |
69 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁)) |
70 | 69, 13 | symgfv 17630 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ 𝐺 ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁)) |
71 | 67, 68, 70 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁)) |
72 | 71 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑄‘𝑗) ∈ (1...𝑁)) |
73 | 4, 5, 47, 48, 49 | minmar1eval 20274 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ (𝑄‘𝑗) ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗)))) |
74 | 64, 65, 66, 65, 72, 73 | syl122anc 1327 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗)))) |
75 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 = 𝐼) |
76 | 75 | iftrued 4044 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅))) |
77 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (𝑄‘𝑗) = 𝐽) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = (◡𝑄‘𝐽)) |
79 | 69, 13 | symgbasf1o 17626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ 𝐺 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) |
80 | 67, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) |
81 | 80 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) |
82 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 ∈ (1...𝑁)) |
83 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗) |
84 | 81, 82, 83 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗) |
85 | 36 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = (◡𝑄‘𝐽)) |
86 | 26, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁)) |
87 | | madjusmdet.n |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑁 ∈ ℕ) |
88 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
89 | 87, 88 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
90 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
92 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑁)) = 𝑁) |
93 | 86, 91, 92 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = 𝑁) |
94 | 85, 93 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡𝑄‘𝐽) = 𝑁) |
95 | 94 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘𝐽) = 𝑁) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘𝐽) = 𝑁) |
97 | 78, 84, 96 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 = 𝑁) |
98 | 97 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → ((𝑄‘𝑗) = 𝐽 → 𝑗 = 𝑁)) |
99 | 98 | con3d 147 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → (¬ 𝑗 = 𝑁 → ¬ (𝑄‘𝑗) = 𝐽)) |
100 | 99 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ¬ (𝑄‘𝑗) = 𝐽) |
101 | 100 | iffalsed 4047 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
102 | 76, 101 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = (0g‘𝑅)) |
103 | 63, 74, 102 | 3eqtrrd 2649 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (0g‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
104 | 58, 103 | ifeqda 4071 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
105 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁)) |
106 | 105 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑖 ∈ (1...𝑁)) |
107 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑗 ∈ (1...𝑁)) |
108 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V |
109 | 108 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) |
110 | 10 | oveqi 6562 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
112 | 111 | mpt2eq3ia 6618 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
113 | 17, 112 | eqtri 2632 |
. . . . . . . . . . 11
⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
114 | 113 | ovmpt4g 6681 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
115 | 106, 107,
109, 114 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
116 | 104, 115 | ifeqda 4071 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))) |
117 | 116 | mpt2eq3dva 6617 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))) |
118 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
119 | 25 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑃 ∈ 𝐺) |
120 | 69, 13 | symgfv 17630 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁)) |
121 | 119, 105,
120 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁)) |
122 | 24 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈 ∈ 𝐵) |
123 | 4, 118, 5, 121, 71, 122 | matecld 20051 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) ∈ (Base‘𝑅)) |
124 | 4, 118, 5, 19, 18, 123 | matbas2d 20048 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) ∈ 𝐵) |
125 | 17, 124 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
126 | 118, 48 | ringidcl 18391 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
127 | 21, 126 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
128 | | eqid 2610 |
. . . . . . . . 9
⊢
((1...𝑁) matRRep
𝑅) = ((1...𝑁) matRRep 𝑅) |
129 | 4, 5, 128, 49 | marrepval 20187 |
. . . . . . . 8
⊢ (((𝑊 ∈ 𝐵 ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ (𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)))) |
130 | 125, 127,
91, 91, 129 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)))) |
131 | 113 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))) |
132 | 117, 130,
131 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = 𝑊) |
133 | 132 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐷‘𝑊)) |
134 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
((1...𝑁) subMat
𝑅) = ((1...𝑁) subMat 𝑅) |
135 | 4, 134, 5 | submaval 20206 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗))) |
136 | 125, 91, 91, 135 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗))) |
137 | | fzdif2 28939 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
138 | 89, 137 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
139 | | mpt2eq12 6613 |
. . . . . . . . . . 11
⊢
((((1...𝑁) ∖
{𝑁}) = (1...(𝑁 − 1)) ∧ ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) |
140 | 138, 138,
139 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) |
141 | 136, 140 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗))) |
142 | | difssd 3700 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁)) |
143 | 138, 142 | eqsstr3d 3603 |
. . . . . . . . . 10
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
144 | 4, 5 | submabas 20203 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐵 ∧ (1...(𝑁 − 1)) ⊆ (1...𝑁)) → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
145 | 125, 143,
144 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
146 | 141, 145 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
147 | | madjusmdet.e |
. . . . . . . . 9
⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) |
148 | | eqid 2610 |
. . . . . . . . 9
⊢
((1...(𝑁 − 1))
Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅) |
149 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) |
150 | 147, 148,
149, 118 | mdetcl 20221 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) |
151 | 18, 146, 150 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) |
152 | 118, 16, 48 | ringlidm 18394 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) |
153 | 21, 151, 152 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((1r‘𝑅)
·
(𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) |
154 | 4 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(Base‘𝐴) =
(Base‘((1...𝑁) Mat
𝑅)) |
155 | 5, 154 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘((1...𝑁) Mat 𝑅)) |
156 | 125, 155 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) |
157 | | smadiadetr 20300 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) ∧ (𝑁 ∈ (1...𝑁) ∧ (1r‘𝑅) ∈ (Base‘𝑅))) → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
158 | 18, 156, 91, 127, 157 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
159 | 6 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) |
160 | 16 | oveqi 6562 |
. . . . . . . . 9
⊢
((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) |
161 | 159, 160 | eqeq12i 2624 |
. . . . . . . 8
⊢ ((𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) ↔ (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
162 | 158, 161 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
163 | 138 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅)) |
164 | 163, 147 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸) |
165 | 164 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) |
166 | 165 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 →
((1r‘𝑅)
·
((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
167 | 162, 166 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))) |
168 | 4, 5 | submat1n 29199 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) |
169 | 87, 125, 168 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) |
170 | 169 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝐸‘(𝑁(subMat1‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) |
171 | 153, 167,
170 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) |
172 | 133, 171 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) |
173 | 4, 5, 87, 3, 2, 21, 1, 10 | submatminr1 29204 |
. . . . . 6
⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽)) |
174 | | madjusmdetlem1.3 |
. . . . . 6
⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) |
175 | 173, 174 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) |
176 | 175 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁))) |
177 | 172, 176 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) |
178 | 177 | oveq2d 6565 |
. 2
⊢ (𝜑 → ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) |
179 | 12, 27, 178 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) |