Step | Hyp | Ref
| Expression |
1 | | scmatid.e |
. . . 4
⊢ 𝐸 = (Base‘𝑅) |
2 | | scmatid.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | scmatid.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2738 |
. . . 4
⊢
(1r‘𝐴) = (1r‘𝐴) |
5 | | eqid 2738 |
. . . 4
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
6 | | scmatid.s |
. . . 4
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
7 | 1, 2, 3, 4, 5, 6 | scmatel 21654 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))))) |
8 | 1, 2, 3, 4, 5, 6 | scmatel 21654 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐵 ∧ ∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))))) |
9 | | oveq12 7284 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) = ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
10 | 9 | adantll 711 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) ∧ 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) = ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
11 | | simp-4l 780 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
12 | | simplr 766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) → 𝑑 ∈ 𝐸) |
13 | 12 | anim1ci 616 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → (𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸)) |
14 | | scmatid.0 |
. . . . . . . . . . . . . . . . 17
⊢ 0 =
(0g‘𝑅) |
15 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝐴) = (.r‘𝐴) |
17 | 2, 1, 14, 4, 5, 15, 16 | scmatscmiddistr 21657 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸)) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
18 | 11, 13, 17 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
19 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
20 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → 𝑅 ∈ Ring) |
21 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → 𝑐 ∈ 𝐸) |
22 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸) → 𝑑 ∈ 𝐸) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → 𝑑 ∈ 𝐸) |
24 | 1, 15 | ringcl 19800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸) → (𝑐(.r‘𝑅)𝑑) ∈ 𝐸) |
25 | 20, 21, 23, 24 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → (𝑐(.r‘𝑅)𝑑) ∈ 𝐸) |
26 | 2 | matring 21592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
27 | 3, 4 | ringidcl 19807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐵) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → (1r‘𝐴) ∈ 𝐵) |
30 | 1, 2, 3, 5 | matvscl 21580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑐(.r‘𝑅)𝑑) ∈ 𝐸 ∧ (1r‘𝐴) ∈ 𝐵)) → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵) |
31 | 19, 25, 29, 30 | syl12anc 834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵) |
32 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = (𝑐(.r‘𝑅)𝑑) → (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
33 | 32 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 = (𝑐(.r‘𝑅)𝑑) → (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) ↔ ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)))) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) ∧ 𝑒 = (𝑐(.r‘𝑅)𝑑)) → (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) ↔ ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)))) |
35 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
36 | 25, 34, 35 | rspcedvd 3563 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → ∃𝑒 ∈ 𝐸 ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))) |
37 | 1, 2, 3, 4, 5, 6 | scmatel 21654 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆 ↔ (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵 ∧ ∃𝑒 ∈ 𝐸 ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))))) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆 ↔ (((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵 ∧ ∃𝑒 ∈ 𝐸 ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))))) |
39 | 31, 36, 38 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸)) → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆) |
40 | 39 | exp32 421 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑑 ∈ 𝐸 → (𝑐 ∈ 𝐸 → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵) → (𝑑 ∈ 𝐸 → (𝑐 ∈ 𝐸 → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆))) |
42 | 41 | imp 407 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) → (𝑐 ∈ 𝐸 → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆)) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) → (𝑐 ∈ 𝐸 → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆)) |
44 | 43 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → ((𝑐(.r‘𝑅)𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆) |
45 | 18, 44 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) ∈ 𝑆) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) ∧ 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) ∈ 𝑆) |
47 | 46 | adantr 481 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) ∧ 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(.r‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) ∈ 𝑆) |
48 | 10, 47 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) ∧ 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆) |
49 | 48 | exp31 420 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) ∧ 𝑐 ∈ 𝐸) → (𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
50 | 49 | rexlimdva 3213 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) ∧ 𝑋 ∈ 𝐵) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
51 | 50 | expimpd 454 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
52 | 51 | com23 86 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵) ∧ 𝑑 ∈ 𝐸) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
53 | 52 | rexlimdva 3213 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐵) → (∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
54 | 53 | expimpd 454 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑌 ∈ 𝐵 ∧ ∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
55 | 8, 54 | sylbid 239 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌 ∈ 𝑆 → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
56 | 55 | com23 86 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑋 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑌 ∈ 𝑆 → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
57 | 7, 56 | sylbid 239 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ 𝑆 → (𝑌 ∈ 𝑆 → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆))) |
58 | 57 | imp32 419 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆) |