Proof of Theorem pmatcollpwscmatlem1
Step | Hyp | Ref
| Expression |
1 | | pmatcollpwscmat.m2 |
. . . . . . . 8
⊢ 𝑀 = (𝑄 ∗ 1 ) |
2 | 1 | oveqi 6562 |
. . . . . . 7
⊢ (𝑎𝑀𝑏) = (𝑎(𝑄 ∗ 1 )𝑏) |
3 | | pmatcollpwscmat.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
4 | 3 | ply1ring 19439 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
5 | 4 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring)) |
6 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸) → 𝑄 ∈ 𝐸) |
7 | 5, 6 | anim12i 588 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ 𝑄 ∈ 𝐸)) |
8 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸) ↔ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ 𝑄 ∈ 𝐸)) |
9 | 7, 8 | sylibr 223 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸)) |
10 | | pmatcollpwscmat.c |
. . . . . . . . 9
⊢ 𝐶 = (𝑁 Mat 𝑃) |
11 | | pmatcollpwscmat.e2 |
. . . . . . . . 9
⊢ 𝐸 = (Base‘𝑃) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
13 | | pmatcollpwscmat.1 |
. . . . . . . . 9
⊢ 1 =
(1r‘𝐶) |
14 | | pmatcollpwscmat.m1 |
. . . . . . . . 9
⊢ ∗ = (
·𝑠 ‘𝐶) |
15 | 10, 11, 12, 13, 14 | scmatscmide 20132 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0g‘𝑃))) |
16 | 9, 15 | sylan 487 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0g‘𝑃))) |
17 | 2, 16 | syl5eq 2656 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) = if(𝑎 = 𝑏, 𝑄, (0g‘𝑃))) |
18 | 17 | fveq2d 6107 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (coe1‘(𝑎𝑀𝑏)) = (coe1‘if(𝑎 = 𝑏, 𝑄, (0g‘𝑃)))) |
19 | 18 | fveq1d 6105 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ((coe1‘(𝑎𝑀𝑏))‘𝐿) = ((coe1‘if(𝑎 = 𝑏, 𝑄, (0g‘𝑃)))‘𝐿)) |
20 | | fvif 6114 |
. . . . . 6
⊢
(coe1‘if(𝑎 = 𝑏, 𝑄, (0g‘𝑃))) = if(𝑎 = 𝑏, (coe1‘𝑄),
(coe1‘(0g‘𝑃))) |
21 | 20 | fveq1i 6104 |
. . . . 5
⊢
((coe1‘if(𝑎 = 𝑏, 𝑄, (0g‘𝑃)))‘𝐿) = (if(𝑎 = 𝑏, (coe1‘𝑄),
(coe1‘(0g‘𝑃)))‘𝐿) |
22 | | iffv 6115 |
. . . . 5
⊢ (if(𝑎 = 𝑏, (coe1‘𝑄),
(coe1‘(0g‘𝑃)))‘𝐿) = if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿)) |
23 | 21, 22 | eqtri 2632 |
. . . 4
⊢
((coe1‘if(𝑎 = 𝑏, 𝑄, (0g‘𝑃)))‘𝐿) = if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿)) |
24 | 19, 23 | syl6eq 2660 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ((coe1‘(𝑎𝑀𝑏))‘𝐿) = if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿))) |
25 | 24 | oveq1d 6564 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
26 | | ovif 6635 |
. . 3
⊢ (if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))),
(((coe1‘(0g‘𝑃))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
27 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
28 | 3, 12, 27 | coe1z 19454 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
29 | 28 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
30 | 29 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((coe1‘(0g‘𝑃))‘𝐿) = ((ℕ0 ×
{(0g‘𝑅)})‘𝐿)) |
31 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝑅)
∈ V) |
33 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸) → 𝐿 ∈
ℕ0) |
34 | 32, 33 | anim12i 588 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((0g‘𝑅)
∈ V ∧ 𝐿 ∈
ℕ0)) |
35 | | fvconst2g 6372 |
. . . . . . . . 9
⊢
(((0g‘𝑅) ∈ V ∧ 𝐿 ∈ ℕ0) →
((ℕ0 × {(0g‘𝑅)})‘𝐿) = (0g‘𝑅)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → ((ℕ0
× {(0g‘𝑅)})‘𝐿) = (0g‘𝑅)) |
37 | 30, 36 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((coe1‘(0g‘𝑃))‘𝐿) = (0g‘𝑅)) |
38 | 37 | oveq1d 6564 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((coe1‘(0g‘𝑃))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘𝑅)(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
39 | 3 | ply1lmod 19443 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
40 | 39 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → 𝑃 ∈ LMod) |
41 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
42 | 41 | ringmgp 18376 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
43 | 4, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
44 | | 0nn0 11184 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
45 | 44 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 0 ∈
ℕ0) |
46 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(var1‘𝑅) = (var1‘𝑅) |
47 | 46, 3, 11 | vr1cl 19408 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ 𝐸) |
48 | 41, 11 | mgpbas 18318 |
. . . . . . . . . . 11
⊢ 𝐸 =
(Base‘(mulGrp‘𝑃)) |
49 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
50 | 48, 49 | mulgnn0cl 17381 |
. . . . . . . . . 10
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ 0 ∈ ℕ0 ∧
(var1‘𝑅)
∈ 𝐸) →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝐸) |
51 | 43, 45, 47, 50 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝐸) |
52 | 51 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝐸) |
53 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
54 | | eqid 2610 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
55 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
56 | 11, 53, 54, 55, 12 | lmod0vs 18719 |
. . . . . . . 8
⊢ ((𝑃 ∈ LMod ∧
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝐸) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
57 | 40, 52, 56 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
58 | 3 | ply1sca 19444 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
59 | 58 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃)) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
61 | 60 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((0g‘𝑅)(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
62 | 61 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(((0g‘𝑅)(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃) ↔
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃))) |
63 | 62 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((0g‘𝑅)(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃) ↔
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃))) |
64 | 57, 63 | mpbird 246 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((0g‘𝑅)(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
65 | 38, 64 | eqtrd 2644 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((coe1‘(0g‘𝑃))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
66 | 65 | ifeq2d 4055 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))),
(((coe1‘(0g‘𝑃))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))), (0g‘𝑃))) |
67 | 66 | adantr 480 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))),
(((coe1‘(0g‘𝑃))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))), (0g‘𝑃))) |
68 | 26, 67 | syl5eq 2656 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (if(𝑎 = 𝑏, ((coe1‘𝑄)‘𝐿),
((coe1‘(0g‘𝑃))‘𝐿))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))), (0g‘𝑃))) |
69 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸)) |
70 | 69 | ancomd 466 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑄 ∈ 𝐸 ∧ 𝐿 ∈
ℕ0)) |
71 | | eqid 2610 |
. . . . . . . . 9
⊢
(coe1‘𝑄) = (coe1‘𝑄) |
72 | | pmatcollpwscmat.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
73 | 71, 11, 3, 72 | coe1fvalcl 19403 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0) →
((coe1‘𝑄)‘𝐿) ∈ 𝐾) |
74 | 70, 73 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((coe1‘𝑄)‘𝐿) ∈ 𝐾) |
75 | 58 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(Scalar‘𝑃) = 𝑅) |
76 | 75 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝑃) = 𝑅) |
77 | 76 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
78 | 77, 72 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝑃)) = 𝐾) |
79 | 78 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(((coe1‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔
((coe1‘𝑄)‘𝐿) ∈ 𝐾)) |
80 | 79 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((coe1‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔
((coe1‘𝑄)‘𝐿) ∈ 𝐾)) |
81 | 74, 80 | mpbird 246 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
((coe1‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃))) |
82 | | pmatcollpwscmat.u |
. . . . . . 7
⊢ 𝑈 = (algSc‘𝑃) |
83 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
84 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑃) = (1r‘𝑃) |
85 | 82, 53, 83, 54, 84 | asclval 19156 |
. . . . . 6
⊢
(((coe1‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) → (𝑈‘((coe1‘𝑄)‘𝐿)) = (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(1r‘𝑃))) |
86 | 81, 85 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → (𝑈‘((coe1‘𝑄)‘𝐿)) = (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(1r‘𝑃))) |
87 | 3, 46, 41, 49 | ply1idvr1 19484 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (1r‘𝑃)) |
88 | 87 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑃) =
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
89 | 88 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(1r‘𝑃) =
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
90 | 89 | oveq2d 6565 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(1r‘𝑃)) = (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
91 | 86, 90 | eqtr2d 2645 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) →
(((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (𝑈‘((coe1‘𝑄)‘𝐿))) |
92 | 91 | ifeq1d 4054 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) → if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))), (0g‘𝑃)) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |
93 | 92 | adantr 480 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → if(𝑎 = 𝑏, (((coe1‘𝑄)‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))), (0g‘𝑃)) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |
94 | 25, 68, 93 | 3eqtrd 2648 |
1
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0
∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) |