Step | Hyp | Ref
| Expression |
1 | | mat2pmatbas.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
3 | 1, 2 | matmulr 20063 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
4 | 3 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(.r‘𝐴) =
(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)) |
5 | 4 | oveqdr 6573 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑥(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑦)) |
6 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
7 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
8 | | crngring 18381 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
9 | 8 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
10 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
11 | | mat2pmatbas.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝐴) |
12 | 11 | eleq2i 2680 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐴)) |
13 | 12 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ (Base‘𝐴)) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ (Base‘𝐴)) |
15 | 14 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (Base‘𝐴)) |
16 | 1, 6 | matbas2 20046 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑𝑚 (𝑁 × 𝑁)) = (Base‘𝐴)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) = (Base‘𝐴)) |
18 | 15, 17 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
19 | 11 | eleq2i 2680 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐴)) |
20 | 19 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘𝐴)) |
21 | 20 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘𝐴)) |
22 | 16 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴))) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴))) |
24 | 21, 23 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
25 | 2, 6, 7, 9, 10, 10, 10, 18, 24 | mamuval 20011 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
26 | 5, 25 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
27 | 26 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
28 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝑖𝑥𝑚) = (𝑘𝑥𝑚)) |
29 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → (𝑚𝑦𝑗) = (𝑚𝑦𝑙)) |
30 | 28, 29 | oveqan12d 6568 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)) = ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) |
31 | 30 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) |
32 | 31 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
33 | 32 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑙)) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
34 | | simp2 1055 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
35 | | simp3 1056 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
36 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑅 Σg
(𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) ∈ V |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) ∈ V) |
38 | 27, 33, 34, 35, 37 | ovmpt2d 6686 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑘(𝑥(.r‘𝐴)𝑦)𝑙) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
39 | 38 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))) |
40 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
41 | | ringcmn 18404 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
42 | 8, 41 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd) |
43 | 42 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CMnd) |
44 | 43 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ CMnd) |
45 | | mat2pmatbas.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
46 | 45 | ply1ring 19439 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
47 | 8, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
48 | | ringmnd 18379 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Mnd) |
50 | 49 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Mnd) |
51 | 50 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑃 ∈ Mnd) |
52 | 10 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑁 ∈ Fin) |
53 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
54 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
55 | 47 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) |
56 | 45 | ply1lmod 19443 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
57 | 8, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑃 ∈ LMod) |
58 | 57 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ LMod) |
59 | 53, 54, 55, 58 | asclghm 19159 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
((Scalar‘𝑃) GrpHom
𝑃)) |
60 | 45 | ply1sca 19444 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
61 | 60 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃)) |
62 | 61 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 GrpHom 𝑃) = ((Scalar‘𝑃) GrpHom 𝑃)) |
63 | 59, 62 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 GrpHom 𝑃)) |
64 | | ghmmhm 17493 |
. . . . . . . . . 10
⊢
((algSc‘𝑃)
∈ (𝑅 GrpHom 𝑃) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 MndHom 𝑃)) |
66 | 65 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
67 | 66 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
68 | 9 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ Ring) |
69 | 68 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑅 ∈ Ring) |
70 | 34 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
71 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ 𝑁) |
72 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴)) |
73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴)) |
74 | 73, 12 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ 𝐵) |
75 | 1, 6, 11, 70, 71, 74 | matecld 20051 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑘𝑥𝑚) ∈ (Base‘𝑅)) |
76 | 35 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
77 | 1 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
78 | 11, 77 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
79 | 78 | eleq2i 2680 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
80 | 79 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
81 | 80 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
82 | 81 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
83 | 82 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
84 | 83, 79 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
85 | 1, 6, 11, 71, 76, 84 | matecld 20051 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅)) |
86 | 6, 7 | ringcl 18384 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅)) |
87 | 69, 75, 85, 86 | syl3anc 1318 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅)) |
88 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) |
89 | | ovex 6577 |
. . . . . . . . 9
⊢ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ V |
90 | 89 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ V) |
91 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑅) ∈ V |
92 | 91 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
93 | 88, 52, 90, 92 | fsuppmptdm 8169 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) finSupp (0g‘𝑅)) |
94 | 6, 40, 44, 51, 52, 67, 87, 93 | gsummptmhm 18163 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))) |
95 | 45 | ply1assa 19390 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) |
97 | 53, 54 | asclrhm 19163 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ AssAlg →
(algSc‘𝑃) ∈
((Scalar‘𝑃) RingHom
𝑃)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
((Scalar‘𝑃) RingHom
𝑃)) |
99 | 61 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
100 | 98, 99 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 RingHom 𝑃)) |
101 | 100 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
102 | 101 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
103 | 102 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
104 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴)) |
105 | 104 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴)) |
106 | 105, 19 | sylibr 223 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
107 | 1, 6, 11, 71, 76, 106 | matecld 20051 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅)) |
108 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
109 | 6, 7, 108 | rhmmul 18550 |
. . . . . . . . 9
⊢
(((algSc‘𝑃)
∈ (𝑅 RingHom 𝑃) ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))) |
110 | 103, 75, 107, 109 | syl3anc 1318 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))) |
111 | 110 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) = (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))) |
112 | 111 | oveq2d 6565 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))) |
113 | 39, 94, 112 | 3eqtr2d 2650 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))) |
114 | 113 | mpt2eq3dva 6617 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))) |
115 | | mat2pmatbas.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
116 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
117 | | eqid 2610 |
. . . . 5
⊢
(.r‘𝐶) = (.r‘𝐶) |
118 | 47 | ad2antlr 759 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Ring) |
119 | | eqid 2610 |
. . . . 5
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
120 | | eqid 2610 |
. . . . 5
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
121 | 9 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
122 | | simp2 1055 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
123 | | simp3 1056 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
124 | | simp1rl 1119 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑥 ∈ 𝐵) |
125 | 1, 6, 11, 122, 123, 124 | matecld 20051 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑥𝑗) ∈ (Base‘𝑅)) |
126 | 45, 53, 6, 116 | ply1sclcl 19477 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑥𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃)) |
127 | 121, 125,
126 | syl2anc 691 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃)) |
128 | | simp1rr 1120 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
129 | 1, 6, 11, 122, 123, 128 | matecld 20051 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑦𝑗) ∈ (Base‘𝑅)) |
130 | 45, 53, 6, 116 | ply1sclcl 19477 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑦𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃)) |
131 | 121, 129,
130 | syl2anc 691 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃)) |
132 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → (𝑘𝑥𝑚) = (𝑖𝑥𝑗)) |
133 | 132 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
134 | 133 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
135 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → (𝑚𝑦𝑙) = (𝑖𝑦𝑗)) |
136 | 135 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
137 | 136 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
138 | | fvex 6113 |
. . . . . 6
⊢
((algSc‘𝑃)‘(𝑘𝑥𝑚)) ∈ V |
139 | 138 | a1i 11 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) ∈ V) |
140 | | fvex 6113 |
. . . . . 6
⊢
((algSc‘𝑃)‘(𝑚𝑦𝑙)) ∈ V |
141 | 140 | a1i 11 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) ∈ V) |
142 | 115, 116,
117, 108, 118, 10, 119, 120, 127, 131, 134, 137, 139, 141 | mpt2matmul 20071 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))) |
143 | 114, 142 | eqtr4d 2647 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))) |
144 | 1 | matring 20068 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
145 | 8, 144 | sylan2 490 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
146 | 145 | anim1i 590 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
147 | | 3anass 1035 |
. . . . . 6
⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
148 | 146, 147 | sylibr 223 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
149 | | eqid 2610 |
. . . . . 6
⊢
(.r‘𝐴) = (.r‘𝐴) |
150 | 11, 149 | ringcl 18384 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) |
151 | 148, 150 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) |
152 | | mat2pmatbas.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
153 | 152, 1, 11, 45, 53 | mat2pmatval 20348 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)))) |
154 | 10, 9, 151, 153 | syl3anc 1318 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)))) |
155 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
156 | 155 | anim2i 591 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵)) |
157 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵)) |
158 | 156, 157 | sylibr 223 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵)) |
159 | 152, 1, 11, 45, 53 | mat2pmatval 20348 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))) |
160 | 158, 159 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))) |
161 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
162 | 161 | anim2i 591 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵)) |
163 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵)) |
164 | 162, 163 | sylibr 223 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵)) |
165 | 152, 1, 11, 45, 53 | mat2pmatval 20348 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) |
166 | 164, 165 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) |
167 | 160, 166 | oveq12d 6567 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))) |
168 | 143, 154,
167 | 3eqtr4d 2654 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦))) |
169 | 168 | ralrimivva 2954 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦))) |