Proof of Theorem isassad
Step | Hyp | Ref
| Expression |
1 | | isassad.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ LMod) |
2 | | isassad.2 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Ring) |
3 | 1, 2 | jca 510 |
. 2
⊢ (𝜑 → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring)) |
4 | | isassad.4 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))) |
5 | | isassad.5 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) |
6 | 4, 5 | jca 510 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) |
7 | 6 | ralrimivvva 3193 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) |
8 | | isassad.b |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐹)) |
9 | | isassad.f |
. . . . . 6
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) |
10 | 9 | fveq2d 6900 |
. . . . 5
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(Scalar‘𝑊))) |
11 | 8, 10 | eqtrd 2765 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊))) |
12 | | isassad.v |
. . . . 5
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) |
13 | | isassad.t |
. . . . . . . . 9
⊢ (𝜑 → × =
(.r‘𝑊)) |
14 | | isassad.s |
. . . . . . . . . 10
⊢ (𝜑 → · = (
·𝑠 ‘𝑊)) |
15 | 14 | oveqd 7436 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 · 𝑥) = (𝑟( ·𝑠
‘𝑊)𝑥)) |
16 | | eqidd 2726 |
. . . . . . . . 9
⊢ (𝜑 → 𝑦 = 𝑦) |
17 | 13, 15, 16 | oveq123d 7440 |
. . . . . . . 8
⊢ (𝜑 → ((𝑟 · 𝑥) × 𝑦) = ((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦)) |
18 | | eqidd 2726 |
. . . . . . . . 9
⊢ (𝜑 → 𝑟 = 𝑟) |
19 | 13 | oveqd 7436 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 × 𝑦) = (𝑥(.r‘𝑊)𝑦)) |
20 | 14, 18, 19 | oveq123d 7440 |
. . . . . . . 8
⊢ (𝜑 → (𝑟 · (𝑥 × 𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))) |
21 | 17, 20 | eqeq12d 2741 |
. . . . . . 7
⊢ (𝜑 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)))) |
22 | | eqidd 2726 |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 = 𝑥) |
23 | 14 | oveqd 7436 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 · 𝑦) = (𝑟( ·𝑠
‘𝑊)𝑦)) |
24 | 13, 22, 23 | oveq123d 7440 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 × (𝑟 · 𝑦)) = (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦))) |
25 | 24, 20 | eqeq12d 2741 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)))) |
26 | 21, 25 | anbi12d 630 |
. . . . . 6
⊢ (𝜑 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
27 | 12, 26 | raleqbidv 3329 |
. . . . 5
⊢ (𝜑 → (∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
28 | 12, 27 | raleqbidv 3329 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
29 | 11, 28 | raleqbidv 3329 |
. . 3
⊢ (𝜑 → (∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
30 | 7, 29 | mpbid 231 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)))) |
31 | | eqid 2725 |
. . 3
⊢
(Base‘𝑊) =
(Base‘𝑊) |
32 | | eqid 2725 |
. . 3
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
33 | | eqid 2725 |
. . 3
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
34 | | eqid 2725 |
. . 3
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
35 | | eqid 2725 |
. . 3
⊢
(.r‘𝑊) = (.r‘𝑊) |
36 | 31, 32, 33, 34, 35 | isassa 21807 |
. 2
⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧
∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑦)) = (𝑟( ·𝑠
‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
37 | 3, 30, 36 | sylanbrc 581 |
1
⊢ (𝜑 → 𝑊 ∈ AssAlg) |