| 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 21877 | . . 3
⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 7 | 6 | simprbi 496 | . 2
⊢ (𝑊 ∈ AssAlg →
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) | 
| 8 |  | oveq1 7439 | . . . . . 6
⊢ (𝑟 = 𝐴 → (𝑟 · 𝑥) = (𝐴 · 𝑥)) | 
| 9 | 8 | oveq1d 7447 | . . . . 5
⊢ (𝑟 = 𝐴 → ((𝑟 · 𝑥) × 𝑦) = ((𝐴 · 𝑥) × 𝑦)) | 
| 10 |  | oveq1 7439 | . . . . 5
⊢ (𝑟 = 𝐴 → (𝑟 · (𝑥 × 𝑦)) = (𝐴 · (𝑥 × 𝑦))) | 
| 11 | 9, 10 | eqeq12d 2752 | . . . 4
⊢ (𝑟 = 𝐴 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)))) | 
| 12 |  | oveq1 7439 | . . . . . 6
⊢ (𝑟 = 𝐴 → (𝑟 · 𝑦) = (𝐴 · 𝑦)) | 
| 13 | 12 | oveq2d 7448 | . . . . 5
⊢ (𝑟 = 𝐴 → (𝑥 × (𝑟 · 𝑦)) = (𝑥 × (𝐴 · 𝑦))) | 
| 14 | 13, 10 | eqeq12d 2752 | . . . 4
⊢ (𝑟 = 𝐴 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)))) | 
| 15 | 11, 14 | anbi12d 632 | . . 3
⊢ (𝑟 = 𝐴 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))))) | 
| 16 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝐴 · 𝑥) = (𝐴 · 𝑋)) | 
| 17 | 16 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝐴 · 𝑥) × 𝑦) = ((𝐴 · 𝑋) × 𝑦)) | 
| 18 |  | oveq1 7439 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 × 𝑦) = (𝑋 × 𝑦)) | 
| 19 | 18 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑋 → (𝐴 · (𝑥 × 𝑦)) = (𝐴 · (𝑋 × 𝑦))) | 
| 20 | 17, 19 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑋 → (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)))) | 
| 21 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑦))) | 
| 22 | 21, 19 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑋 → ((𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)))) | 
| 23 | 20, 22 | anbi12d 632 | . . 3
⊢ (𝑥 = 𝑋 → ((((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))))) | 
| 24 |  | oveq2 7440 | . . . . 5
⊢ (𝑦 = 𝑌 → ((𝐴 · 𝑋) × 𝑦) = ((𝐴 · 𝑋) × 𝑌)) | 
| 25 |  | oveq2 7440 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋 × 𝑦) = (𝑋 × 𝑌)) | 
| 26 | 25 | oveq2d 7448 | . . . . 5
⊢ (𝑦 = 𝑌 → (𝐴 · (𝑋 × 𝑦)) = (𝐴 · (𝑋 × 𝑌))) | 
| 27 | 24, 26 | eqeq12d 2752 | . . . 4
⊢ (𝑦 = 𝑌 → (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))) | 
| 28 |  | oveq2 7440 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝐴 · 𝑦) = (𝐴 · 𝑌)) | 
| 29 | 28 | oveq2d 7448 | . . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑌))) | 
| 30 | 29, 26 | eqeq12d 2752 | . . . 4
⊢ (𝑦 = 𝑌 → ((𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) | 
| 31 | 27, 30 | anbi12d 632 | . . 3
⊢ (𝑦 = 𝑌 → ((((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))) | 
| 32 | 15, 23, 31 | rspc3v 3637 | . 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))) | 
| 33 | 7, 32 | mpan9 506 | 1
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) |