Proof of Theorem madjusmdetlem3
Step | Hyp | Ref
| Expression |
1 | | madjusmdet.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
4 | | fzdif2 28939 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
6 | | difss 3699 |
. . . . . . . . 9
⊢
((1...𝑁) ∖
{𝑁}) ⊆ (1...𝑁) |
7 | 5, 6 | syl6eqssr 3619 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
9 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ (1...(𝑁 − 1))) |
10 | 8, 9 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ (1...𝑁)) |
11 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ (1...(𝑁 − 1))) |
12 | 8, 11 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ (1...𝑁)) |
13 | | ovex 6577 |
. . . . . . 7
⊢ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗)) ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗)) ∈ V) |
15 | | madjusmdetlem3.w |
. . . . . . 7
⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) |
16 | 15 | ovmpt4g 6681 |
. . . . . 6
⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) |
17 | 10, 12, 14, 16 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖𝑊𝑗) = (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) |
18 | 9, 11 | ovresd 6699 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))𝑗) = (𝑖𝑊𝑗)) |
19 | | eqid 2610 |
. . . . . . 7
⊢ (𝐼(subMat1‘𝑈)𝐽) = (𝐼(subMat1‘𝑈)𝐽) |
20 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑁 ∈ ℕ) |
21 | | madjusmdet.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) |
22 | 21 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝐼 ∈ (1...𝑁)) |
23 | | madjusmdet.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝐽 ∈ (1...𝑁)) |
25 | | madjusmdetlem3.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
26 | | madjusmdet.a |
. . . . . . . . . 10
⊢ 𝐴 = ((1...𝑁) Mat 𝑅) |
27 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
28 | | madjusmdet.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐴) |
29 | 26, 27, 28 | matbas2i 20047 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐵 → 𝑈 ∈ ((Base‘𝑅) ↑𝑚 ((1...𝑁) × (1...𝑁)))) |
30 | 25, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ ((Base‘𝑅) ↑𝑚 ((1...𝑁) × (1...𝑁)))) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑈 ∈ ((Base‘𝑅) ↑𝑚 ((1...𝑁) × (1...𝑁)))) |
32 | | fz1ssnn 12243 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
33 | 32, 10 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑖 ∈ ℕ) |
34 | 32, 12 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → 𝑗 ∈ ℕ) |
35 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = if(𝑖 < 𝐼, 𝑖, (𝑖 + 1))) |
36 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑗 < 𝐽, 𝑗, (𝑗 + 1)) = if(𝑗 < 𝐽, 𝑗, (𝑗 + 1))) |
37 | 19, 20, 20, 22, 24, 31, 33, 34, 35, 36 | smatlem 29191 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1))𝑈if(𝑗 < 𝐽, 𝑗, (𝑗 + 1)))) |
38 | | madjusmdet.d |
. . . . . . . . 9
⊢ 𝐷 = ((1...𝑁) maDet 𝑅) |
39 | | madjusmdet.k |
. . . . . . . . 9
⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) |
40 | | madjusmdet.t |
. . . . . . . . 9
⊢ · =
(.r‘𝑅) |
41 | | madjusmdet.z |
. . . . . . . . 9
⊢ 𝑍 = (ℤRHom‘𝑅) |
42 | | madjusmdet.e |
. . . . . . . . 9
⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) |
43 | | madjusmdet.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ CRing) |
44 | | madjusmdet.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ 𝐵) |
45 | | madjusmdetlem2.p |
. . . . . . . . 9
⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) |
46 | | madjusmdetlem2.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) |
47 | 28, 26, 38, 39, 40, 41, 42, 1, 43, 21, 21, 44, 45, 46 | madjusmdetlem2 29222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑁 − 1))) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑖)) |
48 | 9, 47 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑖 < 𝐼, 𝑖, (𝑖 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑖)) |
49 | | madjusmdetlem4.q |
. . . . . . . . 9
⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) |
50 | | madjusmdetlem4.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) |
51 | 28, 26, 38, 39, 40, 41, 42, 1, 43, 23, 23, 44, 49, 50 | madjusmdetlem2 29222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 − 1))) → if(𝑗 < 𝐽, 𝑗, (𝑗 + 1)) = ((𝑄 ∘ ◡𝑇)‘𝑗)) |
52 | 11, 51 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → if(𝑗 < 𝐽, 𝑗, (𝑗 + 1)) = ((𝑄 ∘ ◡𝑇)‘𝑗)) |
53 | 48, 52 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (if(𝑖 < 𝐼, 𝑖, (𝑖 + 1))𝑈if(𝑗 < 𝐽, 𝑗, (𝑗 + 1))) = (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) |
54 | 37, 53 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) |
55 | 17, 18, 54 | 3eqtr4rd 2655 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (1...(𝑁 − 1)) ∧ 𝑗 ∈ (1...(𝑁 − 1)))) → (𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (𝑖(𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))𝑗)) |
56 | 55 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (𝑖(𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))𝑗)) |
57 | | eqid 2610 |
. . . . 5
⊢
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) |
58 | 26, 28, 57, 19, 1, 21, 23, 25 | smatcl 29196 |
. . . 4
⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
59 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
60 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) = (1...𝑁) |
61 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁)) |
62 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁))) |
63 | 60, 45, 61, 62 | fzto1st 29184 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
64 | 21, 63 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
65 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
66 | 3, 65 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
67 | 60, 46, 61, 62 | fzto1st 29184 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
69 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(invg‘(SymGrp‘(1...𝑁))) =
(invg‘(SymGrp‘(1...𝑁))) |
70 | 61, 62, 69 | symginv 17645 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(Base‘(SymGrp‘(1...𝑁))) →
((invg‘(SymGrp‘(1...𝑁)))‘𝑆) = ◡𝑆) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((invg‘(SymGrp‘(1...𝑁)))‘𝑆) = ◡𝑆) |
72 | 61 | symggrp 17643 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑁) ∈ Fin
→ (SymGrp‘(1...𝑁)) ∈ Grp) |
73 | 59, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp) |
74 | 62, 69 | grpinvcl 17290 |
. . . . . . . . . . . . . 14
⊢
(((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) →
((invg‘(SymGrp‘(1...𝑁)))‘𝑆) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
75 | 73, 68, 74 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((invg‘(SymGrp‘(1...𝑁)))‘𝑆) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
76 | 71, 75 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
77 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(+g‘(SymGrp‘(1...𝑁))) =
(+g‘(SymGrp‘(1...𝑁))) |
78 | 61, 62, 77 | symgov 17633 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+g‘(SymGrp‘(1...𝑁)))◡𝑆) = (𝑃 ∘ ◡𝑆)) |
79 | 61, 62, 77 | symgcl 17634 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+g‘(SymGrp‘(1...𝑁)))◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁)))) |
80 | 78, 79 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃 ∘ ◡𝑆) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
81 | 64, 76, 80 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ∘ ◡𝑆) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
82 | 81 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃 ∘ ◡𝑆) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
83 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁)) |
84 | 61, 62 | symgfv 17630 |
. . . . . . . . . 10
⊢ (((𝑃 ∘ ◡𝑆) ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑃 ∘ ◡𝑆)‘𝑖) ∈ (1...𝑁)) |
85 | 82, 83, 84 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃 ∘ ◡𝑆)‘𝑖) ∈ (1...𝑁)) |
86 | 60, 49, 61, 62 | fzto1st 29184 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (1...𝑁) → 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
87 | 23, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
88 | 60, 50, 61, 62 | fzto1st 29184 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
89 | 66, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
90 | 61, 62, 69 | symginv 17645 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈
(Base‘(SymGrp‘(1...𝑁))) →
((invg‘(SymGrp‘(1...𝑁)))‘𝑇) = ◡𝑇) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((invg‘(SymGrp‘(1...𝑁)))‘𝑇) = ◡𝑇) |
92 | 62, 69 | grpinvcl 17290 |
. . . . . . . . . . . . . 14
⊢
(((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) →
((invg‘(SymGrp‘(1...𝑁)))‘𝑇) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
93 | 73, 89, 92 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((invg‘(SymGrp‘(1...𝑁)))‘𝑇) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
94 | 91, 93 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
95 | 61, 62, 77 | symgov 17633 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+g‘(SymGrp‘(1...𝑁)))◡𝑇) = (𝑄 ∘ ◡𝑇)) |
96 | 61, 62, 77 | symgcl 17634 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+g‘(SymGrp‘(1...𝑁)))◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁)))) |
97 | 95, 96 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ ◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄 ∘ ◡𝑇) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
98 | 87, 94, 97 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 ∘ ◡𝑇) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
99 | 98 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄 ∘ ◡𝑇) ∈
(Base‘(SymGrp‘(1...𝑁)))) |
100 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) |
101 | 61, 62 | symgfv 17630 |
. . . . . . . . . 10
⊢ (((𝑄 ∘ ◡𝑇) ∈
(Base‘(SymGrp‘(1...𝑁))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑄 ∘ ◡𝑇)‘𝑗) ∈ (1...𝑁)) |
102 | 99, 100, 101 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑄 ∘ ◡𝑇)‘𝑗) ∈ (1...𝑁)) |
103 | 25 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈 ∈ 𝐵) |
104 | 26, 27, 28, 85, 102, 103 | matecld 20051 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗)) ∈ (Base‘𝑅)) |
105 | 26, 27, 28, 59, 43, 104 | matbas2d 20048 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) ∈ 𝐵) |
106 | 15, 105 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
107 | 26, 28 | submatres 29200 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) |
108 | 1, 106, 107 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) |
109 | | eqid 2610 |
. . . . . 6
⊢ (𝑁(subMat1‘𝑊)𝑁) = (𝑁(subMat1‘𝑊)𝑁) |
110 | 26, 28, 57, 109, 1, 66, 66, 106 | smatcl 29196 |
. . . . 5
⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
111 | 108, 110 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) ∈
(Base‘((1...(𝑁
− 1)) Mat 𝑅))) |
112 | | eqid 2610 |
. . . . 5
⊢
((1...(𝑁 − 1))
Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅) |
113 | 112, 57 | eqmat 20049 |
. . . 4
⊢ (((𝐼(subMat1‘𝑈)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) ∧ (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) ∈
(Base‘((1...(𝑁
− 1)) Mat 𝑅))) →
((𝐼(subMat1‘𝑈)𝐽) = (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) ↔ ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (𝑖(𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))𝑗))) |
114 | 58, 111, 113 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐼(subMat1‘𝑈)𝐽) = (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))) ↔ ∀𝑖 ∈ (1...(𝑁 − 1))∀𝑗 ∈ (1...(𝑁 − 1))(𝑖(𝐼(subMat1‘𝑈)𝐽)𝑗) = (𝑖(𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))𝑗))) |
115 | 56, 114 | mpbird 246 |
. 2
⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑊 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) |
116 | 115, 108 | eqtr4d 2647 |
1
⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) |