Proof of Theorem ascldimulOLD
Step | Hyp | Ref
| Expression |
1 | | assaring 20093 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
2 | | eqid 2821 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) |
3 | | eqid 2821 |
. . . . . . . . 9
⊢
(1r‘𝑊) = (1r‘𝑊) |
4 | 2, 3 | ringidcl 19318 |
. . . . . . . 8
⊢ (𝑊 ∈ Ring →
(1r‘𝑊)
∈ (Base‘𝑊)) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg →
(1r‘𝑊)
∈ (Base‘𝑊)) |
6 | | ascldimul.t |
. . . . . . . 8
⊢ × =
(.r‘𝑊) |
7 | 2, 6, 3 | ringlidm 19321 |
. . . . . . 7
⊢ ((𝑊 ∈ Ring ∧
(1r‘𝑊)
∈ (Base‘𝑊))
→ ((1r‘𝑊) ×
(1r‘𝑊)) =
(1r‘𝑊)) |
8 | 1, 5, 7 | syl2anc 586 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg →
((1r‘𝑊)
×
(1r‘𝑊)) =
(1r‘𝑊)) |
9 | 8 | oveq2d 7172 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → (𝑆(
·𝑠 ‘𝑊)((1r‘𝑊) ×
(1r‘𝑊))) =
(𝑆(
·𝑠 ‘𝑊)(1r‘𝑊))) |
10 | 9 | oveq2d 7172 |
. . . 4
⊢ (𝑊 ∈ AssAlg → (𝑅(
·𝑠 ‘𝑊)(𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊))))
= (𝑅(
·𝑠 ‘𝑊)(𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
11 | 10 | 3ad2ant1 1129 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝑅( ·𝑠
‘𝑊)(𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊))))
= (𝑅(
·𝑠 ‘𝑊)(𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
12 | | simp1 1132 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → 𝑊 ∈ AssAlg) |
13 | | simp2 1133 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → 𝑅 ∈ 𝐾) |
14 | 5 | 3ad2ant1 1129 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (1r‘𝑊) ∈ (Base‘𝑊)) |
15 | | assalmod 20092 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
16 | 15 | 3ad2ant1 1129 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → 𝑊 ∈ LMod) |
17 | | simp3 1134 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → 𝑆 ∈ 𝐾) |
18 | | ascldimul.f |
. . . . . . 7
⊢ 𝐹 = (Scalar‘𝑊) |
19 | | eqid 2821 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
20 | | ascldimul.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝐹) |
21 | 2, 18, 19, 20 | lmodvscl 19651 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝐾 ∧ (1r‘𝑊) ∈ (Base‘𝑊)) → (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊)) |
22 | 16, 17, 14, 21 | syl3anc 1367 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊)) |
23 | 2, 18, 20, 19, 6 | assaass 20090 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝑅 ∈ 𝐾 ∧ (1r‘𝑊) ∈ (Base‘𝑊) ∧ (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)) ∈ (Base‘𝑊))) → ((𝑅( ·𝑠
‘𝑊)(1r‘𝑊)) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑅( ·𝑠
‘𝑊)((1r‘𝑊) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))))) |
24 | 12, 13, 14, 22, 23 | syl13anc 1368 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((𝑅( ·𝑠
‘𝑊)(1r‘𝑊)) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑅( ·𝑠
‘𝑊)((1r‘𝑊) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))))) |
25 | 2, 18, 20, 19, 6 | assaassr 20091 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝑆 ∈ 𝐾 ∧ (1r‘𝑊) ∈ (Base‘𝑊) ∧
(1r‘𝑊)
∈ (Base‘𝑊)))
→ ((1r‘𝑊) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊)))) |
26 | 12, 17, 14, 14, 25 | syl13anc 1368 |
. . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((1r‘𝑊) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊)))) |
27 | 26 | oveq2d 7172 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝑅( ·𝑠
‘𝑊)((1r‘𝑊) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) = (𝑅( ·𝑠
‘𝑊)(𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊))))) |
28 | 24, 27 | eqtrd 2856 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((𝑅( ·𝑠
‘𝑊)(1r‘𝑊)) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) = (𝑅( ·𝑠
‘𝑊)(𝑆( ·𝑠
‘𝑊)((1r‘𝑊) ×
(1r‘𝑊))))) |
29 | | ascldimul.s |
. . . . 5
⊢ · =
(.r‘𝐹) |
30 | 2, 18, 19, 20, 29 | lmodvsass 19659 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾 ∧ (1r‘𝑊) ∈ (Base‘𝑊))) → ((𝑅 · 𝑆)( ·𝑠
‘𝑊)(1r‘𝑊)) = (𝑅( ·𝑠
‘𝑊)(𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
31 | 16, 13, 17, 14, 30 | syl13anc 1368 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((𝑅 · 𝑆)( ·𝑠
‘𝑊)(1r‘𝑊)) = (𝑅( ·𝑠
‘𝑊)(𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
32 | 11, 28, 31 | 3eqtr4rd 2867 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((𝑅 · 𝑆)( ·𝑠
‘𝑊)(1r‘𝑊)) = ((𝑅( ·𝑠
‘𝑊)(1r‘𝑊)) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
33 | 18 | assasca 20094 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ CRing) |
34 | | crngring 19308 |
. . . . 5
⊢ (𝐹 ∈ CRing → 𝐹 ∈ Ring) |
35 | 33, 34 | syl 17 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ Ring) |
36 | 20, 29 | ringcl 19311 |
. . . 4
⊢ ((𝐹 ∈ Ring ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝑅 · 𝑆) ∈ 𝐾) |
37 | 35, 36 | syl3an1 1159 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝑅 · 𝑆) ∈ 𝐾) |
38 | | ascldimul.a |
. . . 4
⊢ 𝐴 = (algSc‘𝑊) |
39 | 38, 18, 20, 19, 3 | asclval 20109 |
. . 3
⊢ ((𝑅 · 𝑆) ∈ 𝐾 → (𝐴‘(𝑅 · 𝑆)) = ((𝑅 · 𝑆)( ·𝑠
‘𝑊)(1r‘𝑊))) |
40 | 37, 39 | syl 17 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘(𝑅 · 𝑆)) = ((𝑅 · 𝑆)( ·𝑠
‘𝑊)(1r‘𝑊))) |
41 | 38, 18, 20, 19, 3 | asclval 20109 |
. . . 4
⊢ (𝑅 ∈ 𝐾 → (𝐴‘𝑅) = (𝑅( ·𝑠
‘𝑊)(1r‘𝑊))) |
42 | 13, 41 | syl 17 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘𝑅) = (𝑅( ·𝑠
‘𝑊)(1r‘𝑊))) |
43 | 38, 18, 20, 19, 3 | asclval 20109 |
. . . 4
⊢ (𝑆 ∈ 𝐾 → (𝐴‘𝑆) = (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) |
44 | 17, 43 | syl 17 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘𝑆) = (𝑆( ·𝑠
‘𝑊)(1r‘𝑊))) |
45 | 42, 44 | oveq12d 7174 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → ((𝐴‘𝑅) × (𝐴‘𝑆)) = ((𝑅( ·𝑠
‘𝑊)(1r‘𝑊)) × (𝑆( ·𝑠
‘𝑊)(1r‘𝑊)))) |
46 | 32, 40, 45 | 3eqtr4d 2866 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘(𝑅 · 𝑆)) = ((𝐴‘𝑅) × (𝐴‘𝑆))) |