| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 2 | | smatvscl.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐴) =
(Base‘𝐴) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(1r‘𝐴) = (1r‘𝐴) |
| 5 | | smatvscl.t |
. . . . 5
⊢ ∗ = (
·𝑠 ‘𝐴) |
| 6 | | smatvscl.s |
. . . . 5
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
| 7 | 1, 2, 3, 4, 5, 6 | scmatel 22511 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑋 = (𝑐 ∗
(1r‘𝐴))))) |
| 8 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑋 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 ∗ 𝑋) = (𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))) |
| 9 | 8 | adantl 481 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∗ 𝑋) = (𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))) |
| 10 | 2 | matlmod 22435 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
| 11 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝐴 ∈ LMod) |
| 12 | | smatvscl.k |
. . . . . . . . . . . . . . . . 17
⊢ 𝐾 = (Base‘𝑅) |
| 13 | 2 | matsca2 22426 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝐴))) |
| 15 | 12, 14 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐾 =
(Base‘(Scalar‘𝐴))) |
| 16 | 15 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐶 ∈ 𝐾 ↔ 𝐶 ∈ (Base‘(Scalar‘𝐴)))) |
| 17 | 16 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → 𝐶 ∈ (Base‘(Scalar‘𝐴))) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝐶 ∈ (Base‘(Scalar‘𝐴))) |
| 19 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) → 𝑅 = (Scalar‘𝐴)) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) → (Base‘𝑅) = (Base‘(Scalar‘𝐴))) |
| 21 | 20 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) → (𝑐 ∈ (Base‘𝑅) ↔ 𝑐 ∈ (Base‘(Scalar‘𝐴)))) |
| 22 | 21 | biimpa 476 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝑐 ∈ (Base‘(Scalar‘𝐴))) |
| 23 | 2 | matring 22449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 24 | 3, 4 | ringidcl 20262 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ (Base‘𝐴)) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ (Base‘𝐴)) |
| 26 | 25 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (1r‘𝐴) ∈ (Base‘𝐴)) |
| 27 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
| 29 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘(Scalar‘𝐴)) =
(.r‘(Scalar‘𝐴)) |
| 30 | 3, 27, 5, 28, 29 | lmodvsass 20885 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ LMod ∧ (𝐶 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑐 ∈ (Base‘(Scalar‘𝐴)) ∧
(1r‘𝐴)
∈ (Base‘𝐴)))
→ ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))) |
| 31 | 11, 18, 22, 26, 30 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))) |
| 32 | 31 | eqcomd 2743 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝐶 ∗ (𝑐 ∗
(1r‘𝐴))) =
((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))) |
| 33 | | simplll 775 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
| 34 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → 𝑅 = (Scalar‘𝐴)) |
| 35 | 34 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → (Scalar‘𝐴) = 𝑅) |
| 36 | 35 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (Scalar‘𝐴) = 𝑅) |
| 37 | 36 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) →
(.r‘(Scalar‘𝐴)) = (.r‘𝑅)) |
| 38 | 37 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝐶(.r‘(Scalar‘𝐴))𝑐) = (𝐶(.r‘𝑅)𝑐)) |
| 39 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 40 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝐶 ∈ 𝐾) |
| 41 | 12 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘𝑅) =
𝐾 |
| 42 | 41 | eleq2i 2833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ (Base‘𝑅) ↔ 𝑐 ∈ 𝐾) |
| 43 | 42 | biimpi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ (Base‘𝑅) → 𝑐 ∈ 𝐾) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → 𝑐 ∈ 𝐾) |
| 45 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 46 | 12, 45 | ringcl 20247 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾) → (𝐶(.r‘𝑅)𝑐) ∈ 𝐾) |
| 47 | 39, 40, 44, 46 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝐶(.r‘𝑅)𝑐) ∈ 𝐾) |
| 48 | 38, 47 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝐶(.r‘(Scalar‘𝐴))𝑐) ∈ 𝐾) |
| 49 | 12, 2, 3, 5 | matvscl 22437 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∈ 𝐾 ∧ (1r‘𝐴) ∈ (Base‘𝐴))) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ (Base‘𝐴)) |
| 50 | 33, 48, 26, 49 | syl12anc 837 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ (Base‘𝐴)) |
| 51 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶(.r‘(Scalar‘𝐴))𝑐) = 𝑒 → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))) |
| 52 | 51 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = (𝐶(.r‘(Scalar‘𝐴))𝑐) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑒 = (𝐶(.r‘(Scalar‘𝐴))𝑐)) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))) |
| 54 | 48, 53 | rspcedeq2vd 3630 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → ∃𝑒 ∈ 𝐾 ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))) |
| 55 | 12, 2, 3, 4, 5, 6 | scmatel 22511 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ 𝑆 ↔ (((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ (Base‘𝐴) ∧
∃𝑒 ∈ 𝐾 ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))))) |
| 56 | 55 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ 𝑆 ↔ (((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ (Base‘𝐴) ∧
∃𝑒 ∈ 𝐾 ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴)) =
(𝑒 ∗
(1r‘𝐴))))) |
| 57 | 50, 54, 56 | mpbir2and 713 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐶(.r‘(Scalar‘𝐴))𝑐) ∗
(1r‘𝐴))
∈ 𝑆) |
| 58 | 32, 57 | eqeltrd 2841 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) → (𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))
∈ 𝑆) |
| 59 | 58 | adantr 480 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∗ (𝑐 ∗
(1r‘𝐴)))
∈ 𝑆) |
| 60 | 9, 59 | eqeltrd 2841 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ 𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∗ 𝑋) ∈ 𝑆) |
| 61 | 60 | rexlimdva2 3157 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑋 ∈ (Base‘𝐴)) → (∃𝑐 ∈ (Base‘𝑅)𝑋 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 ∗ 𝑋) ∈ 𝑆)) |
| 62 | 61 | expimpd 453 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → ((𝑋 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∗ 𝑋) ∈ 𝑆)) |
| 63 | 62 | ex 412 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐶 ∈ 𝐾 → ((𝑋 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∗ 𝑋) ∈ 𝑆))) |
| 64 | 63 | com23 86 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑋 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)𝑋 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 ∈ 𝐾 → (𝐶 ∗ 𝑋) ∈ 𝑆))) |
| 65 | 7, 64 | sylbid 240 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ 𝑆 → (𝐶 ∈ 𝐾 → (𝐶 ∗ 𝑋) ∈ 𝑆))) |
| 66 | 65 | com23 86 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐶 ∈ 𝐾 → (𝑋 ∈ 𝑆 → (𝐶 ∗ 𝑋) ∈ 𝑆))) |
| 67 | 66 | imp32 418 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆) |