Step | Hyp | Ref
| Expression |
1 | | mdetmptr12.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
2 | | mdetmptr12.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ Fin) |
3 | | mdetmptr12.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ 𝐵) |
4 | | mdetmptr12.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐺) |
5 | | mdetpmtr.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
6 | | mdetpmtr.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
7 | | mdetpmtr.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
8 | | mdetpmtr.g |
. . . 4
⊢ 𝐺 =
(Base‘(SymGrp‘𝑁)) |
9 | | mdetpmtr.s |
. . . 4
⊢ 𝑆 = (pmSgn‘𝑁) |
10 | | mdetpmtr.z |
. . . 4
⊢ 𝑍 = (ℤRHom‘𝑅) |
11 | | mdetpmtr.t |
. . . 4
⊢ · =
(.r‘𝑅) |
12 | | fveq2 6771 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝑃‘𝑘) = (𝑃‘𝑖)) |
13 | 12 | oveq1d 7286 |
. . . . 5
⊢ (𝑘 = 𝑖 → ((𝑃‘𝑘)𝑀𝑙) = ((𝑃‘𝑖)𝑀𝑙)) |
14 | | oveq2 7279 |
. . . . 5
⊢ (𝑙 = 𝑗 → ((𝑃‘𝑖)𝑀𝑙) = ((𝑃‘𝑖)𝑀𝑗)) |
15 | 13, 14 | cbvmpov 7364 |
. . . 4
⊢ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) |
16 | 5, 6, 7, 8, 9, 10,
11, 15 | mdetpmtr1 31769 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))))) |
17 | 1, 2, 3, 4, 16 | syl22anc 836 |
. 2
⊢ (𝜑 → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))))) |
18 | | eqid 2740 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
19 | 4 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
20 | | simp2 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
21 | | eqid 2740 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
22 | 21, 8 | symgfv 18985 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁) |
23 | 19, 20, 22 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁) |
24 | | simp3 1137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
25 | 3 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
26 | 5, 18, 6, 23, 24, 25 | matecld 21573 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑙) ∈ (Base‘𝑅)) |
27 | 5, 18, 6, 2, 1, 26 | matbas2d 21570 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)) ∈ 𝐵) |
28 | | mdetmptr12.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐺) |
29 | | eqid 2740 |
. . . . . 6
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗))) |
30 | 5, 6, 7, 8, 9, 10,
11, 29 | mdetpmtr2 31770 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ ((𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)) ∈ 𝐵 ∧ 𝑄 ∈ 𝐺)) → (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))) = (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)))))) |
31 | 1, 2, 27, 28, 30 | syl22anc 836 |
. . . 4
⊢ (𝜑 → (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))) = (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)))))) |
32 | | mdetpmtr12.e |
. . . . . . 7
⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) |
33 | | simp2 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
34 | 28 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑄 ∈ 𝐺) |
35 | | simp3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
36 | 21, 8 | symgfv 18985 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ 𝐺 ∧ 𝑗 ∈ 𝑁) → (𝑄‘𝑗) ∈ 𝑁) |
37 | 34, 35, 36 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑄‘𝑗) ∈ 𝑁) |
38 | | oveq2 7279 |
. . . . . . . . . 10
⊢ (𝑙 = (𝑄‘𝑗) → ((𝑃‘𝑖)𝑀𝑙) = ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) |
39 | | eqid 2740 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)) |
40 | | ovex 7304 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑖)𝑀(𝑄‘𝑗)) ∈ V |
41 | 13, 38, 39, 40 | ovmpo 7427 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝑁 ∧ (𝑄‘𝑗) ∈ 𝑁) → (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)) = ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) |
42 | 33, 37, 41 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)) = ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) |
43 | 42 | mpoeq3dva 7346 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗)))) |
44 | 32, 43 | eqtr4id 2799 |
. . . . . 6
⊢ (𝜑 → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)))) |
45 | 44 | fveq2d 6775 |
. . . . 5
⊢ (𝜑 → (𝐷‘𝐸) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗))))) |
46 | 45 | oveq2d 7287 |
. . . 4
⊢ (𝜑 → (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))(𝑄‘𝑗)))))) |
47 | 31, 46 | eqtr4d 2783 |
. . 3
⊢ (𝜑 → (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙))) = (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸))) |
48 | 47 | oveq2d 7287 |
. 2
⊢ (𝜑 → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑙)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸)))) |
49 | | crngring 19793 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
50 | 1, 49 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
51 | 8, 9, 10 | zrhcopsgnelbas 20798 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
52 | 50, 2, 4, 51 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅)) |
53 | 8, 9, 10 | zrhcopsgnelbas 20798 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅)) |
54 | 50, 2, 28, 53 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑍 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅)) |
55 | 4 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺) |
56 | 21, 8 | symgfv 18985 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
57 | 55, 33, 56 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁) |
58 | 3 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
59 | 5, 18, 6, 57, 37, 58 | matecld 21573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀(𝑄‘𝑗)) ∈ (Base‘𝑅)) |
60 | 5, 18, 6, 2, 1, 59 | matbas2d 21570 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) ∈ 𝐵) |
61 | 32, 60 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝐵) |
62 | 7, 5, 6, 18 | mdetcl 21743 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝐵) → (𝐷‘𝐸) ∈ (Base‘𝑅)) |
63 | 1, 61, 62 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐸) ∈ (Base‘𝑅)) |
64 | 18, 11 | ringass 19801 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅) ∧ (𝐷‘𝐸) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑄)) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸)))) |
65 | 50, 52, 54, 63, 64 | syl13anc 1371 |
. . 3
⊢ (𝜑 → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑄)) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸)))) |
66 | 8, 9 | cofipsgn 20796 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
67 | 2, 4, 66 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃))) |
68 | 8, 9 | cofipsgn 20796 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑄) = (𝑍‘(𝑆‘𝑄))) |
69 | 2, 28, 68 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑍 ∘ 𝑆)‘𝑄) = (𝑍‘(𝑆‘𝑄))) |
70 | 67, 69 | oveq12d 7289 |
. . . . 5
⊢ (𝜑 → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑄)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑄)))) |
71 | 10 | zrhrhm 20711 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring
RingHom 𝑅)) |
72 | 50, 71 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (ℤring RingHom
𝑅)) |
73 | | 1z 12350 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
74 | | neg1z 12356 |
. . . . . . . 8
⊢ -1 ∈
ℤ |
75 | | prssi 4760 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆
ℤ) |
76 | 73, 74, 75 | mp2an 689 |
. . . . . . 7
⊢ {1, -1}
⊆ ℤ |
77 | 8, 9 | psgnran 19121 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1}) |
78 | 2, 4, 77 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝑃) ∈ {1, -1}) |
79 | 76, 78 | sselid 3924 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝑃) ∈ ℤ) |
80 | 8, 9 | psgnran 19121 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺) → (𝑆‘𝑄) ∈ {1, -1}) |
81 | 2, 28, 80 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝑄) ∈ {1, -1}) |
82 | 76, 81 | sselid 3924 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝑄) ∈ ℤ) |
83 | | zringbas 20674 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
84 | | zringmulr 20677 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
85 | 83, 84, 11 | rhmmul 19969 |
. . . . . 6
⊢ ((𝑍 ∈ (ℤring
RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑄) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑄)))) |
86 | 72, 79, 82, 85 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑄)))) |
87 | 70, 86 | eqtr4d 2783 |
. . . 4
⊢ (𝜑 → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑄)) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄)))) |
88 | 87 | oveq1d 7286 |
. . 3
⊢ (𝜑 → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑄)) · (𝐷‘𝐸)) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) |
89 | 65, 88 | eqtr3d 2782 |
. 2
⊢ (𝜑 → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑄) · (𝐷‘𝐸))) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) |
90 | 17, 48, 89 | 3eqtrd 2784 |
1
⊢ (𝜑 → (𝐷‘𝑀) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) |