Step | Hyp | Ref
| Expression |
1 | | isassa.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | | isassa.f |
. . . 4
⊢ 𝐹 = (Scalar‘𝑊) |
3 | | isassa.b |
. . . 4
⊢ 𝐵 = (Base‘𝐹) |
4 | | isassa.s |
. . . 4
⊢ · = (
·𝑠 ‘𝑊) |
5 | | isassa.t |
. . . 4
⊢ × =
(.r‘𝑊) |
6 | 1, 2, 3, 4, 5 | isassa 20818 |
. . 3
⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) |
7 | 6 | simprbi 500 |
. 2
⊢ (𝑊 ∈ AssAlg →
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) |
8 | | oveq1 7220 |
. . . . . 6
⊢ (𝑟 = 𝐴 → (𝑟 · 𝑥) = (𝐴 · 𝑥)) |
9 | 8 | oveq1d 7228 |
. . . . 5
⊢ (𝑟 = 𝐴 → ((𝑟 · 𝑥) × 𝑦) = ((𝐴 · 𝑥) × 𝑦)) |
10 | | oveq1 7220 |
. . . . 5
⊢ (𝑟 = 𝐴 → (𝑟 · (𝑥 × 𝑦)) = (𝐴 · (𝑥 × 𝑦))) |
11 | 9, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑟 = 𝐴 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)))) |
12 | | oveq1 7220 |
. . . . . 6
⊢ (𝑟 = 𝐴 → (𝑟 · 𝑦) = (𝐴 · 𝑦)) |
13 | 12 | oveq2d 7229 |
. . . . 5
⊢ (𝑟 = 𝐴 → (𝑥 × (𝑟 · 𝑦)) = (𝑥 × (𝐴 · 𝑦))) |
14 | 13, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑟 = 𝐴 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)))) |
15 | 11, 14 | anbi12d 634 |
. . 3
⊢ (𝑟 = 𝐴 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))))) |
16 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝐴 · 𝑥) = (𝐴 · 𝑋)) |
17 | 16 | oveq1d 7228 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝐴 · 𝑥) × 𝑦) = ((𝐴 · 𝑋) × 𝑦)) |
18 | | oveq1 7220 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 × 𝑦) = (𝑋 × 𝑦)) |
19 | 18 | oveq2d 7229 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐴 · (𝑥 × 𝑦)) = (𝐴 · (𝑋 × 𝑦))) |
20 | 17, 19 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑋 → (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)))) |
21 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑦))) |
22 | 21, 19 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)))) |
23 | 20, 22 | anbi12d 634 |
. . 3
⊢ (𝑥 = 𝑋 → ((((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))))) |
24 | | oveq2 7221 |
. . . . 5
⊢ (𝑦 = 𝑌 → ((𝐴 · 𝑋) × 𝑦) = ((𝐴 · 𝑋) × 𝑌)) |
25 | | oveq2 7221 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋 × 𝑦) = (𝑋 × 𝑌)) |
26 | 25 | oveq2d 7229 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝐴 · (𝑋 × 𝑦)) = (𝐴 · (𝑋 × 𝑌))) |
27 | 24, 26 | eqeq12d 2753 |
. . . 4
⊢ (𝑦 = 𝑌 → (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))) |
28 | | oveq2 7221 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝐴 · 𝑦) = (𝐴 · 𝑌)) |
29 | 28 | oveq2d 7229 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑌))) |
30 | 29, 26 | eqeq12d 2753 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) |
31 | 27, 30 | anbi12d 634 |
. . 3
⊢ (𝑦 = 𝑌 → ((((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))) |
32 | 15, 23, 31 | rspc3v 3550 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))) |
33 | 7, 32 | mpan9 510 |
1
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) |