| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing) |
| 2 | | mat2pmatbas.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
| 3 | 2 | ply1assa 22201 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
| 4 | | mat2pmatlin.s |
. . . . . . . . . . 11
⊢ 𝑆 = (algSc‘𝑃) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
| 6 | 4, 5 | asclrhm 21910 |
. . . . . . . . . 10
⊢ (𝑃 ∈ AssAlg → 𝑆 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
| 7 | 1, 3, 6 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑆 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
| 8 | 2 | ply1sca 22254 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
| 9 | 8 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃)) |
| 10 | 9 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
| 11 | 7, 10 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑆 ∈ (𝑅 RingHom 𝑃)) |
| 12 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → 𝑆 ∈ (𝑅 RingHom 𝑃)) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑆 ∈ (𝑅 RingHom 𝑃)) |
| 14 | | mat2pmatlin.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑅) |
| 15 | 14 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐾 ↔ 𝑋 ∈ (Base‘𝑅)) |
| 16 | 15 | biimpi 216 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐾 → 𝑋 ∈ (Base‘𝑅)) |
| 17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑅)) |
| 18 | 17 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑋 ∈ (Base‘𝑅)) |
| 19 | | mat2pmatbas.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 20 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 21 | | mat2pmatbas.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
| 22 | | simprl 771 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
| 23 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
| 24 | 23 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
| 25 | | simplrr 778 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑌 ∈ 𝐵) |
| 26 | 19, 20, 21, 22, 24, 25 | matecld 22432 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖𝑌𝑗) ∈ (Base‘𝑅)) |
| 27 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 28 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 29 | 20, 27, 28 | rhmmul 20486 |
. . . . . 6
⊢ ((𝑆 ∈ (𝑅 RingHom 𝑃) ∧ 𝑋 ∈ (Base‘𝑅) ∧ (𝑖𝑌𝑗) ∈ (Base‘𝑅)) → (𝑆‘(𝑋(.r‘𝑅)(𝑖𝑌𝑗))) = ((𝑆‘𝑋)(.r‘𝑃)(𝑆‘(𝑖𝑌𝑗)))) |
| 30 | 13, 18, 26, 29 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑆‘(𝑋(.r‘𝑅)(𝑖𝑌𝑗))) = ((𝑆‘𝑋)(.r‘𝑃)(𝑆‘(𝑖𝑌𝑗)))) |
| 31 | | crngring 20242 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 32 | 31 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → 𝑅 ∈ Ring) |
| 33 | 32 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) |
| 34 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) |
| 36 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) |
| 37 | | mat2pmatlin.m |
. . . . . . . 8
⊢ · = (
·𝑠 ‘𝐴) |
| 38 | 19, 21, 14, 37, 27 | matvscacell 22442 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑋 · 𝑌)𝑗) = (𝑋(.r‘𝑅)(𝑖𝑌𝑗))) |
| 39 | 33, 35, 36, 38 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑋 · 𝑌)𝑗) = (𝑋(.r‘𝑅)(𝑖𝑌𝑗))) |
| 40 | 39 | fveq2d 6910 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑆‘(𝑖(𝑋 · 𝑌)𝑗)) = (𝑆‘(𝑋(.r‘𝑅)(𝑖𝑌𝑗)))) |
| 41 | 31 | anim2i 617 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
| 42 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
| 43 | 41, 42 | anim12i 613 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵)) |
| 44 | | df-3an 1089 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵)) |
| 45 | 43, 44 | sylibr 234 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵)) |
| 46 | | mat2pmatbas.t |
. . . . . . . 8
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
| 47 | 46, 19, 21, 2, 4 | mat2pmatvalel 22731 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑌)𝑗) = (𝑆‘(𝑖𝑌𝑗))) |
| 48 | 45, 47 | sylan 580 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑌)𝑗) = (𝑆‘(𝑖𝑌𝑗))) |
| 49 | 48 | oveq2d 7447 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑆‘𝑋)(.r‘𝑃)(𝑖(𝑇‘𝑌)𝑗)) = ((𝑆‘𝑋)(.r‘𝑃)(𝑆‘(𝑖𝑌𝑗)))) |
| 50 | 30, 40, 49 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑆‘(𝑖(𝑋 · 𝑌)𝑗)) = ((𝑆‘𝑋)(.r‘𝑃)(𝑖(𝑇‘𝑌)𝑗))) |
| 51 | | simpll 767 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → 𝑁 ∈ Fin) |
| 52 | 51 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑁 ∈ Fin) |
| 53 | 14, 19, 21, 37 | matvscl 22437 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑋 · 𝑌) ∈ 𝐵) |
| 54 | 41, 53 | sylan 580 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑋 · 𝑌) ∈ 𝐵) |
| 55 | 54 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑋 · 𝑌) ∈ 𝐵) |
| 56 | 46, 19, 21, 2, 4 | mat2pmatvalel 22731 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑋 · 𝑌) ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑆‘(𝑖(𝑋 · 𝑌)𝑗))) |
| 57 | 52, 33, 55, 36, 56 | syl31anc 1375 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑆‘(𝑖(𝑋 · 𝑌)𝑗))) |
| 58 | 2 | ply1ring 22249 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 59 | 31, 58 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
| 60 | 59 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → 𝑃 ∈ Ring) |
| 61 | 60 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑃 ∈ Ring) |
| 62 | 31 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
| 63 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐾) |
| 64 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 65 | 2, 4, 14, 64 | ply1sclcl 22289 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → (𝑆‘𝑋) ∈ (Base‘𝑃)) |
| 66 | 62, 63, 65 | syl2an 596 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑆‘𝑋) ∈ (Base‘𝑃)) |
| 67 | | mat2pmatbas.c |
. . . . . . . . 9
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 68 | | mat2pmatbas0.h |
. . . . . . . . 9
⊢ 𝐻 = (Base‘𝐶) |
| 69 | 46, 19, 21, 2, 67, 68 | mat2pmatbas0 22733 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → (𝑇‘𝑌) ∈ 𝐻) |
| 70 | 45, 69 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑇‘𝑌) ∈ 𝐻) |
| 71 | 66, 70 | jca 511 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → ((𝑆‘𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘𝑌) ∈ 𝐻)) |
| 72 | 71 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑆‘𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘𝑌) ∈ 𝐻)) |
| 73 | | mat2pmatlin.n |
. . . . . 6
⊢ × = (
·𝑠 ‘𝐶) |
| 74 | 67, 68, 64, 73, 28 | matvscacell 22442 |
. . . . 5
⊢ ((𝑃 ∈ Ring ∧ ((𝑆‘𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘𝑌) ∈ 𝐻) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗) = ((𝑆‘𝑋)(.r‘𝑃)(𝑖(𝑇‘𝑌)𝑗))) |
| 75 | 61, 72, 36, 74 | syl3anc 1373 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗) = ((𝑆‘𝑋)(.r‘𝑃)(𝑖(𝑇‘𝑌)𝑗))) |
| 76 | 50, 57, 75 | 3eqtr4d 2787 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗)) |
| 77 | 76 | ralrimivva 3202 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗)) |
| 78 | 46, 19, 21, 2, 67, 68 | mat2pmatbas0 22733 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑋 · 𝑌) ∈ 𝐵) → (𝑇‘(𝑋 · 𝑌)) ∈ 𝐻) |
| 79 | 51, 32, 54, 78 | syl3anc 1373 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑇‘(𝑋 · 𝑌)) ∈ 𝐻) |
| 80 | 64, 67, 68, 73 | matvscl 22437 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ ((𝑆‘𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘𝑌) ∈ 𝐻)) → ((𝑆‘𝑋) × (𝑇‘𝑌)) ∈ 𝐻) |
| 81 | 51, 60, 71, 80 | syl21anc 838 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → ((𝑆‘𝑋) × (𝑇‘𝑌)) ∈ 𝐻) |
| 82 | 67, 68 | eqmat 22430 |
. . 3
⊢ (((𝑇‘(𝑋 · 𝑌)) ∈ 𝐻 ∧ ((𝑆‘𝑋) × (𝑇‘𝑌)) ∈ 𝐻) → ((𝑇‘(𝑋 · 𝑌)) = ((𝑆‘𝑋) × (𝑇‘𝑌)) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗))) |
| 83 | 79, 81, 82 | syl2anc 584 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → ((𝑇‘(𝑋 · 𝑌)) = ((𝑆‘𝑋) × (𝑇‘𝑌)) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘(𝑋 · 𝑌))𝑗) = (𝑖((𝑆‘𝑋) × (𝑇‘𝑌))𝑗))) |
| 84 | 77, 83 | mpbird 257 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵)) → (𝑇‘(𝑋 · 𝑌)) = ((𝑆‘𝑋) × (𝑇‘𝑌))) |