| Step | Hyp | Ref
| Expression |
| 1 | | mat2pmatbas.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 2 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
| 3 | 1, 2 | matmulr 22444 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
| 4 | 3 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(.r‘𝐴) =
(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)) |
| 5 | 4 | oveqdr 7459 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑥(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑦)) |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 7 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 8 | | crngring 20242 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 9 | 8 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
| 10 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
| 11 | | mat2pmatbas.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝐴) |
| 12 | 11 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐴)) |
| 13 | 12 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ (Base‘𝐴)) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ (Base‘𝐴)) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (Base‘𝐴)) |
| 16 | 1, 6 | matbas2 22427 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑m (𝑁
× 𝑁)) =
(Base‘𝐴)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴)) |
| 18 | 15, 17 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 19 | 11 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐴)) |
| 20 | 19 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘𝐴)) |
| 21 | 20 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘𝐴)) |
| 22 | 16 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴))) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴))) |
| 24 | 21, 23 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
| 25 | 2, 6, 7, 9, 10, 10, 10, 18, 24 | mamuval 22397 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
| 26 | 5, 25 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
| 27 | 26 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))))) |
| 28 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝑖𝑥𝑚) = (𝑘𝑥𝑚)) |
| 29 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → (𝑚𝑦𝑗) = (𝑚𝑦𝑙)) |
| 30 | 28, 29 | oveqan12d 7450 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)) = ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) |
| 31 | 30 | mpteq2dv 5244 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) |
| 32 | 31 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
| 33 | 32 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑙)) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
| 34 | | simp2 1138 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
| 35 | | simp3 1139 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
| 36 | | ovexd 7466 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) ∈ V) |
| 37 | 27, 33, 34, 35, 36 | ovmpod 7585 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑘(𝑥(.r‘𝐴)𝑦)𝑙) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) |
| 38 | 37 | fveq2d 6910 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))) |
| 39 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 40 | | ringcmn 20279 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 41 | 8, 40 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd) |
| 42 | 41 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CMnd) |
| 43 | 42 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ CMnd) |
| 44 | | mat2pmatbas.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Poly1‘𝑅) |
| 45 | 44 | ply1ring 22249 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 46 | 8, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
| 47 | | ringmnd 20240 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Mnd) |
| 49 | 48 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Mnd) |
| 50 | 49 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑃 ∈ Mnd) |
| 51 | 10 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑁 ∈ Fin) |
| 52 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
| 53 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
| 54 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring) |
| 55 | 44 | ply1lmod 22253 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
| 56 | 8, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑃 ∈ LMod) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ LMod) |
| 58 | 52, 53, 54, 57 | asclghm 21903 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
((Scalar‘𝑃) GrpHom
𝑃)) |
| 59 | 44 | ply1sca 22254 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃)) |
| 61 | 60 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 GrpHom 𝑃) = ((Scalar‘𝑃) GrpHom 𝑃)) |
| 62 | 58, 61 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 GrpHom 𝑃)) |
| 63 | | ghmmhm 19244 |
. . . . . . . . . 10
⊢
((algSc‘𝑃)
∈ (𝑅 GrpHom 𝑃) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 MndHom 𝑃)) |
| 65 | 64 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
| 66 | 65 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃)) |
| 67 | 9 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 68 | 67 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 69 | 34 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
| 70 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ 𝑁) |
| 71 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴)) |
| 72 | 71 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴)) |
| 73 | 72, 12 | sylibr 234 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ 𝐵) |
| 74 | 1, 6, 11, 69, 70, 73 | matecld 22432 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑘𝑥𝑚) ∈ (Base‘𝑅)) |
| 75 | 35 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
| 76 | 1 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
| 77 | 11, 76 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
| 78 | 77 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
| 79 | 78 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
| 80 | 79 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
| 81 | 80 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
| 82 | 81 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅))) |
| 83 | 82, 78 | sylibr 234 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
| 84 | 1, 6, 11, 70, 75, 83 | matecld 22432 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅)) |
| 85 | 6, 7 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅)) |
| 86 | 68, 74, 84, 85 | syl3anc 1373 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅)) |
| 87 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) |
| 88 | | ovexd 7466 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ V) |
| 89 | | fvexd 6921 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
| 90 | 87, 51, 88, 89 | fsuppmptdm 9416 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) finSupp (0g‘𝑅)) |
| 91 | 6, 39, 43, 50, 51, 66, 86, 90 | gsummptmhm 19958 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))) |
| 92 | 44 | ply1assa 22201 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
| 93 | 92 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) |
| 94 | 52, 53 | asclrhm 21910 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ AssAlg →
(algSc‘𝑃) ∈
((Scalar‘𝑃) RingHom
𝑃)) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
((Scalar‘𝑃) RingHom
𝑃)) |
| 96 | 60 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
| 97 | 95, 96 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(algSc‘𝑃) ∈
(𝑅 RingHom 𝑃)) |
| 98 | 97 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
| 99 | 98 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
| 100 | 99 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃)) |
| 101 | 21 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴)) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴)) |
| 103 | 102, 19 | sylibr 234 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
| 104 | 1, 6, 11, 70, 75, 103 | matecld 22432 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅)) |
| 105 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 106 | 6, 7, 105 | rhmmul 20486 |
. . . . . . . . 9
⊢
(((algSc‘𝑃)
∈ (𝑅 RingHom 𝑃) ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))) |
| 107 | 100, 74, 104, 106 | syl3anc 1373 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))) |
| 108 | 107 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) = (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))) |
| 109 | 108 | oveq2d 7447 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))) |
| 110 | 38, 91, 109 | 3eqtr2d 2783 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))) |
| 111 | 110 | mpoeq3dva 7510 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))) |
| 112 | | mat2pmatbas.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 113 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 114 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝐶) = (.r‘𝐶) |
| 115 | 46 | ad2antlr 727 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Ring) |
| 116 | | eqid 2737 |
. . . . 5
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
| 117 | | eqid 2737 |
. . . . 5
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
| 118 | 9 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 119 | | simp2 1138 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
| 120 | | simp3 1139 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
| 121 | | simp1rl 1239 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑥 ∈ 𝐵) |
| 122 | 1, 6, 11, 119, 120, 121 | matecld 22432 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑥𝑗) ∈ (Base‘𝑅)) |
| 123 | 44, 52, 6, 113 | ply1sclcl 22289 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑥𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃)) |
| 124 | 118, 122,
123 | syl2anc 584 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃)) |
| 125 | | simp1rr 1240 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑦 ∈ 𝐵) |
| 126 | 1, 6, 11, 119, 120, 125 | matecld 22432 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑦𝑗) ∈ (Base‘𝑅)) |
| 127 | 44, 52, 6, 113 | ply1sclcl 22289 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑦𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃)) |
| 128 | 118, 126,
127 | syl2anc 584 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃)) |
| 129 | | oveq12 7440 |
. . . . . . 7
⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → (𝑘𝑥𝑚) = (𝑖𝑥𝑗)) |
| 130 | 129 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
| 131 | 130 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
| 132 | | oveq12 7440 |
. . . . . . 7
⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → (𝑚𝑦𝑙) = (𝑖𝑦𝑗)) |
| 133 | 132 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
| 134 | 133 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
| 135 | | fvexd 6921 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) ∈ V) |
| 136 | | fvexd 6921 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) ∈ V) |
| 137 | 112, 113,
114, 105, 115, 10, 116, 117, 124, 128, 131, 134, 135, 136 | mpomatmul 22452 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))) |
| 138 | 111, 137 | eqtr4d 2780 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))) |
| 139 | 1 | matring 22449 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 140 | 8, 139 | sylan2 593 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
| 141 | 140 | anim1i 615 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
| 142 | | 3anass 1095 |
. . . . . 6
⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
| 143 | 141, 142 | sylibr 234 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
| 144 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝐴) = (.r‘𝐴) |
| 145 | 11, 144 | ringcl 20247 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) |
| 146 | 143, 145 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) |
| 147 | | mat2pmatbas.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
| 148 | 147, 1, 11, 44, 52 | mat2pmatval 22730 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)))) |
| 149 | 10, 9, 146, 148 | syl3anc 1373 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)))) |
| 150 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 151 | 150 | anim2i 617 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵)) |
| 152 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵)) |
| 153 | 151, 152 | sylibr 234 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵)) |
| 154 | 147, 1, 11, 44, 52 | mat2pmatval 22730 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))) |
| 155 | 153, 154 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))) |
| 156 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 157 | 156 | anim2i 617 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵)) |
| 158 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵)) |
| 159 | 157, 158 | sylibr 234 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵)) |
| 160 | 147, 1, 11, 44, 52 | mat2pmatval 22730 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) |
| 161 | 159, 160 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) |
| 162 | 155, 161 | oveq12d 7449 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))) |
| 163 | 138, 149,
162 | 3eqtr4d 2787 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦))) |
| 164 | 163 | ralrimivva 3202 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦))) |