Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
2 | | simpr 488 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
3 | 2 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝑅 ∈ Ring) |
4 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸) → 𝑄 ∈ 𝐸) |
5 | 4 | anim2i 620 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑄 ∈ 𝐸)) |
6 | | df-3an 1090 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑄 ∈ 𝐸)) |
7 | 5, 6 | sylibr 237 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸)) |
8 | | pmatcollpwscmat.m2 |
. . . . . . 7
⊢ 𝑀 = (𝑄 ∗ 1 ) |
9 | | pmatcollpwscmat.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
10 | | pmatcollpwscmat.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat 𝑃) |
11 | | pmatcollpwscmat.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐶) |
12 | | pmatcollpwscmat.e2 |
. . . . . . . 8
⊢ 𝐸 = (Base‘𝑃) |
13 | | pmatcollpwscmat.m1 |
. . . . . . . 8
⊢ ∗ = (
·𝑠 ‘𝐶) |
14 | | pmatcollpwscmat.1 |
. . . . . . . 8
⊢ 1 =
(1r‘𝐶) |
15 | 9, 10, 11, 12, 13, 14 | 1pmatscmul 21453 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) → (𝑄 ∗ 1 ) ∈ 𝐵) |
16 | 8, 15 | eqeltrid 2837 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) → 𝑀 ∈ 𝐵) |
17 | 7, 16 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝑀 ∈ 𝐵) |
18 | | simprl 771 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝐿 ∈
ℕ0) |
19 | | pmatcollpwscmat.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
20 | | pmatcollpwscmat.d |
. . . . . 6
⊢ 𝐷 = (Base‘𝐴) |
21 | 9, 10, 11, 19, 20 | decpmatcl 21518 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0) → (𝑀 decompPMat 𝐿) ∈ 𝐷) |
22 | 3, 17, 18, 21 | syl3anc 1372 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑀 decompPMat 𝐿) ∈ 𝐷) |
23 | | df-3an 1090 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑀 decompPMat 𝐿) ∈ 𝐷) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 decompPMat 𝐿) ∈ 𝐷)) |
24 | 1, 22, 23 | sylanbrc 586 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑀 decompPMat 𝐿) ∈ 𝐷)) |
25 | | pmatcollpwscmat.t |
. . . 4
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
26 | | eqid 2738 |
. . . 4
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
27 | 25, 19, 20, 9, 26 | mat2pmatval 21475 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑀 decompPMat 𝐿) ∈ 𝐷) → (𝑇‘(𝑀 decompPMat 𝐿)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖(𝑀 decompPMat 𝐿)𝑗)))) |
28 | 24, 27 | syl 17 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑇‘(𝑀 decompPMat 𝐿)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖(𝑀 decompPMat 𝐿)𝑗)))) |
29 | 3, 17, 18 | 3jca 1129 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈
ℕ0)) |
30 | 29 | 3ad2ant1 1134 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈
ℕ0)) |
31 | | 3simpc 1151 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) |
32 | 9, 10, 11 | decpmate 21517 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝐿 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑀 decompPMat 𝐿)𝑗) = ((coe1‘(𝑖𝑀𝑗))‘𝐿)) |
33 | 30, 31, 32 | syl2anc 587 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑀 decompPMat 𝐿)𝑗) = ((coe1‘(𝑖𝑀𝑗))‘𝐿)) |
34 | 33 | fveq2d 6678 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖(𝑀 decompPMat 𝐿)𝑗)) = ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿))) |
35 | 34 | mpoeq3dva 7245 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖(𝑀 decompPMat 𝐿)𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿)))) |
36 | | simp1lr 1238 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
37 | | simp2 1138 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
38 | | simp3 1139 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
39 | 17 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
40 | 10, 12, 11, 37, 38, 39 | matecld 21177 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑀𝑗) ∈ 𝐸) |
41 | 18 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐿 ∈
ℕ0) |
42 | | eqid 2738 |
. . . . . . 7
⊢
(coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑖𝑀𝑗)) |
43 | | pmatcollpwscmat.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑅) |
44 | 42, 12, 9, 43 | coe1fvalcl 20987 |
. . . . . 6
⊢ (((𝑖𝑀𝑗) ∈ 𝐸 ∧ 𝐿 ∈ ℕ0) →
((coe1‘(𝑖𝑀𝑗))‘𝐿) ∈ 𝐾) |
45 | 40, 41, 44 | syl2anc 587 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝑀𝑗))‘𝐿) ∈ 𝐾) |
46 | | eqid 2738 |
. . . . . 6
⊢
(var1‘𝑅) = (var1‘𝑅) |
47 | | eqid 2738 |
. . . . . 6
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
48 | | eqid 2738 |
. . . . . 6
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
49 | | eqid 2738 |
. . . . . 6
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
50 | 43, 9, 46, 47, 48, 49, 26 | ply1scltm 21056 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑖𝑀𝑗))‘𝐿) ∈ 𝐾) → ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿)) = (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
51 | 36, 45, 50 | syl2anc 587 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿)) = (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
52 | 51 | mpoeq3dva 7245 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
53 | | pmatcollpwscmat.e1 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
54 | | pmatcollpwscmat.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝑅) |
55 | | pmatcollpwscmat.u |
. . . . . . 7
⊢ 𝑈 = (algSc‘𝑃) |
56 | | pmatcollpwscmat.s |
. . . . . . 7
⊢ 𝑆 = (algSc‘𝑃) |
57 | 9, 10, 11, 13, 53, 54, 25, 19, 20, 55, 43, 12, 56, 14, 8 | pmatcollpwscmatlem1 21540 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |
58 | | eqidd 2739 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
59 | | oveq12 7179 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖𝑀𝑗) = (𝑎𝑀𝑏)) |
60 | 59 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑎𝑀𝑏))) |
61 | 60 | fveq1d 6676 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → ((coe1‘(𝑖𝑀𝑗))‘𝐿) = ((coe1‘(𝑎𝑀𝑏))‘𝐿)) |
62 | 61 | oveq1d 7185 |
. . . . . . . 8
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
63 | 62 | adantl 485 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝐿 ∈
ℕ0 ∧ 𝑄
∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
64 | | simprl 771 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁) |
65 | | simprr 773 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁) |
66 | | ovexd 7205 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ V) |
67 | 58, 63, 64, 65, 66 | ovmpod 7317 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))𝑏) = (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
68 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝑁 ∈ Fin) |
69 | 9 | ply1ring 21023 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
70 | 69 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
71 | 70 | adantr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝑃 ∈ Ring) |
72 | | pm3.22 463 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸) → (𝑄 ∈ 𝐸 ∧ 𝐿 ∈
ℕ0)) |
73 | 72 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑄 ∈ 𝐸 ∧ 𝐿 ∈
ℕ0)) |
74 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(coe1‘𝑄) = (coe1‘𝑄) |
75 | 74, 12, 9, 43 | coe1fvalcl 20987 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0) →
((coe1‘𝑄)‘𝐿) ∈ 𝐾) |
76 | 73, 75 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((coe1‘𝑄)‘𝐿) ∈ 𝐾) |
77 | 9, 55, 43, 12 | ply1sclcl 21061 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝑄)‘𝐿) ∈ 𝐾) → (𝑈‘((coe1‘𝑄)‘𝐿)) ∈ 𝐸) |
78 | 3, 76, 77 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑈‘((coe1‘𝑄)‘𝐿)) ∈ 𝐸) |
79 | 68, 71, 78 | 3jca 1129 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ (𝑈‘((coe1‘𝑄)‘𝐿)) ∈ 𝐸)) |
80 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘𝑃) = (0g‘𝑃) |
81 | 10, 12, 80, 14, 13 | scmatscmide 21258 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ (𝑈‘((coe1‘𝑄)‘𝐿)) ∈ 𝐸) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |
82 | 79, 81 | sylan 583 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |
83 | 57, 67, 82 | 3eqtr4d 2783 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))𝑏) = (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏)) |
84 | 83 | ralrimivva 3103 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))𝑏) = (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏)) |
85 | | 0nn0 11991 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
86 | 85 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 0 ∈
ℕ0) |
87 | 43, 9, 46, 47, 48, 49, 12 | ply1tmcl 21047 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑖𝑀𝑗))‘𝐿) ∈ 𝐾 ∧ 0 ∈ ℕ0) →
(((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐸) |
88 | 36, 45, 86, 87 | syl3anc 1372 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐸) |
89 | 10, 12, 11, 68, 71, 88 | matbas2d 21174 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
90 | 9, 10, 11, 12, 13, 14 | 1pmatscmul 21453 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑈‘((coe1‘𝑄)‘𝐿)) ∈ 𝐸) → ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ) ∈ 𝐵) |
91 | 68, 3, 78, 90 | syl3anc 1372 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ) ∈ 𝐵) |
92 | 10, 11 | eqmat 21175 |
. . . . 5
⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵 ∧ ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ) ∈ 𝐵) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))𝑏) = (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏))) |
93 | 89, 91, 92 | syl2anc 587 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))𝑏) = (𝑎((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )𝑏))) |
94 | 84, 93 | mpbird 260 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (((coe1‘(𝑖𝑀𝑗))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )) |
95 | 52, 94 | eqtrd 2773 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((coe1‘(𝑖𝑀𝑗))‘𝐿))) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )) |
96 | 28, 35, 95 | 3eqtrd 2777 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑇‘(𝑀 decompPMat 𝐿)) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )) |