Step | Hyp | Ref
| Expression |
1 | | eqid 2778 |
. 2
⊢
(Base‘𝐹) =
(Base‘𝐹) |
2 | | eqid 2778 |
. 2
⊢
(1r‘𝐹) = (1r‘𝐹) |
3 | | eqid 2778 |
. 2
⊢
(1r‘𝑊) = (1r‘𝑊) |
4 | | eqid 2778 |
. 2
⊢
(.r‘𝐹) = (.r‘𝐹) |
5 | | eqid 2778 |
. 2
⊢
(.r‘𝑊) = (.r‘𝑊) |
6 | | asclrhm.f |
. . . 4
⊢ 𝐹 = (Scalar‘𝑊) |
7 | 6 | assasca 19729 |
. . 3
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ CRing) |
8 | | crngring 18956 |
. . 3
⊢ (𝐹 ∈ CRing → 𝐹 ∈ Ring) |
9 | 7, 8 | syl 17 |
. 2
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ Ring) |
10 | | assaring 19728 |
. 2
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
11 | 1, 2 | ringidcl 18966 |
. . . 4
⊢ (𝐹 ∈ Ring →
(1r‘𝐹)
∈ (Base‘𝐹)) |
12 | | asclrhm.a |
. . . . 5
⊢ 𝐴 = (algSc‘𝑊) |
13 | | eqid 2778 |
. . . . 5
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
14 | 12, 6, 1, 13, 3 | asclval 19743 |
. . . 4
⊢
((1r‘𝐹) ∈ (Base‘𝐹) → (𝐴‘(1r‘𝐹)) = ((1r‘𝐹)(
·𝑠 ‘𝑊)(1r‘𝑊))) |
15 | 9, 11, 14 | 3syl 18 |
. . 3
⊢ (𝑊 ∈ AssAlg → (𝐴‘(1r‘𝐹)) = ((1r‘𝐹)(
·𝑠 ‘𝑊)(1r‘𝑊))) |
16 | | assalmod 19727 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
17 | | eqid 2778 |
. . . . . 6
⊢
(Base‘𝑊) =
(Base‘𝑊) |
18 | 17, 3 | ringidcl 18966 |
. . . . 5
⊢ (𝑊 ∈ Ring →
(1r‘𝑊)
∈ (Base‘𝑊)) |
19 | 10, 18 | syl 17 |
. . . 4
⊢ (𝑊 ∈ AssAlg →
(1r‘𝑊)
∈ (Base‘𝑊)) |
20 | 17, 6, 13, 2 | lmodvs1 19294 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧
(1r‘𝑊)
∈ (Base‘𝑊))
→ ((1r‘𝐹)( ·𝑠
‘𝑊)(1r‘𝑊)) = (1r‘𝑊)) |
21 | 16, 19, 20 | syl2anc 579 |
. . 3
⊢ (𝑊 ∈ AssAlg →
((1r‘𝐹)(
·𝑠 ‘𝑊)(1r‘𝑊)) = (1r‘𝑊)) |
22 | 15, 21 | eqtrd 2814 |
. 2
⊢ (𝑊 ∈ AssAlg → (𝐴‘(1r‘𝐹)) = (1r‘𝑊)) |
23 | 17, 5, 3 | ringlidm 18969 |
. . . . . . . 8
⊢ ((𝑊 ∈ Ring ∧
(1r‘𝑊)
∈ (Base‘𝑊))
→ ((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)) = (1r‘𝑊)) |
24 | 10, 19, 23 | syl2anc 579 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg →
((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)) = (1r‘𝑊)) |
25 | 24 | adantr 474 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)) = (1r‘𝑊)) |
26 | 25 | oveq2d 6940 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑦( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) |
27 | 26 | oveq2d 6940 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)))) = (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)(1r‘𝑊)))) |
28 | | simpl 476 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → 𝑊 ∈ AssAlg) |
29 | | simprl 761 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → 𝑥 ∈ (Base‘𝐹)) |
30 | 19 | adantr 474 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (1r‘𝑊) ∈ (Base‘𝑊)) |
31 | 16 | adantr 474 |
. . . . . . 7
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → 𝑊 ∈ LMod) |
32 | | simprr 763 |
. . . . . . 7
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → 𝑦 ∈ (Base‘𝐹)) |
33 | 17, 6, 13, 1 | lmodvscl 19283 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝐹) ∧
(1r‘𝑊)
∈ (Base‘𝑊))
→ (𝑦(
·𝑠 ‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊)) |
34 | 31, 32, 30, 33 | syl3anc 1439 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑦( ·𝑠
‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊)) |
35 | 17, 6, 1, 13, 5 | assaass 19725 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧
(1r‘𝑊)
∈ (Base‘𝑊) ∧
(𝑦(
·𝑠 ‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊))) → ((𝑥( ·𝑠
‘𝑊)(1r‘𝑊))(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑥( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))))) |
36 | 28, 29, 30, 34, 35 | syl13anc 1440 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((𝑥( ·𝑠
‘𝑊)(1r‘𝑊))(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑥( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))))) |
37 | 17, 6, 1, 13, 5 | assaassr 19726 |
. . . . . . 7
⊢ ((𝑊 ∈ AssAlg ∧ (𝑦 ∈ (Base‘𝐹) ∧
(1r‘𝑊)
∈ (Base‘𝑊) ∧
(1r‘𝑊)
∈ (Base‘𝑊)))
→ ((1r‘𝑊)(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)))) |
38 | 28, 32, 30, 30, 37 | syl13anc 1440 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((1r‘𝑊)(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑦( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊)))) |
39 | 38 | oveq2d 6940 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑥( ·𝑠
‘𝑊)((1r‘𝑊)(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊)))) = (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊))))) |
40 | 36, 39 | eqtrd 2814 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((𝑥( ·𝑠
‘𝑊)(1r‘𝑊))(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)((1r‘𝑊)(.r‘𝑊)(1r‘𝑊))))) |
41 | 17, 6, 13, 1, 4 | lmodvsass 19291 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹) ∧ (1r‘𝑊) ∈ (Base‘𝑊))) → ((𝑥(.r‘𝐹)𝑦)( ·𝑠
‘𝑊)(1r‘𝑊)) = (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)(1r‘𝑊)))) |
42 | 31, 29, 32, 30, 41 | syl13anc 1440 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((𝑥(.r‘𝐹)𝑦)( ·𝑠
‘𝑊)(1r‘𝑊)) = (𝑥( ·𝑠
‘𝑊)(𝑦(
·𝑠 ‘𝑊)(1r‘𝑊)))) |
43 | 27, 40, 42 | 3eqtr4rd 2825 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((𝑥(.r‘𝐹)𝑦)( ·𝑠
‘𝑊)(1r‘𝑊)) = ((𝑥( ·𝑠
‘𝑊)(1r‘𝑊))(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊)))) |
44 | 1, 4 | ringcl 18959 |
. . . . . 6
⊢ ((𝐹 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹)) → (𝑥(.r‘𝐹)𝑦) ∈ (Base‘𝐹)) |
45 | 44 | 3expb 1110 |
. . . . 5
⊢ ((𝐹 ∈ Ring ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑥(.r‘𝐹)𝑦) ∈ (Base‘𝐹)) |
46 | 9, 45 | sylan 575 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝑥(.r‘𝐹)𝑦) ∈ (Base‘𝐹)) |
47 | 12, 6, 1, 13, 3 | asclval 19743 |
. . . 4
⊢ ((𝑥(.r‘𝐹)𝑦) ∈ (Base‘𝐹) → (𝐴‘(𝑥(.r‘𝐹)𝑦)) = ((𝑥(.r‘𝐹)𝑦)( ·𝑠
‘𝑊)(1r‘𝑊))) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝐴‘(𝑥(.r‘𝐹)𝑦)) = ((𝑥(.r‘𝐹)𝑦)( ·𝑠
‘𝑊)(1r‘𝑊))) |
49 | 12, 6, 1, 13, 3 | asclval 19743 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝐹) → (𝐴‘𝑥) = (𝑥( ·𝑠
‘𝑊)(1r‘𝑊))) |
50 | 29, 49 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝐴‘𝑥) = (𝑥( ·𝑠
‘𝑊)(1r‘𝑊))) |
51 | 12, 6, 1, 13, 3 | asclval 19743 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝐹) → (𝐴‘𝑦) = (𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) |
52 | 32, 51 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝐴‘𝑦) = (𝑦( ·𝑠
‘𝑊)(1r‘𝑊))) |
53 | 50, 52 | oveq12d 6942 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → ((𝐴‘𝑥)(.r‘𝑊)(𝐴‘𝑦)) = ((𝑥( ·𝑠
‘𝑊)(1r‘𝑊))(.r‘𝑊)(𝑦( ·𝑠
‘𝑊)(1r‘𝑊)))) |
54 | 43, 48, 53 | 3eqtr4d 2824 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐹))) → (𝐴‘(𝑥(.r‘𝐹)𝑦)) = ((𝐴‘𝑥)(.r‘𝑊)(𝐴‘𝑦))) |
55 | 12, 6, 10, 16 | asclghm 19746 |
. 2
⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 GrpHom 𝑊)) |
56 | 1, 2, 3, 4, 5, 9, 10, 22, 54, 55 | isrhm2d 19128 |
1
⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 RingHom 𝑊)) |