| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvexd 6921 | . . . 4
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V) | 
| 2 |  | fveq2 6906 | . . . . 5
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) | 
| 3 |  | isassa.f | . . . . 5
⊢ 𝐹 = (Scalar‘𝑊) | 
| 4 | 2, 3 | eqtr4di 2795 | . . . 4
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) | 
| 5 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑓 = 𝐹 → (Base‘𝑓) = (Base‘𝐹)) | 
| 6 |  | isassa.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐹) | 
| 7 | 5, 6 | eqtr4di 2795 | . . . . . 6
⊢ (𝑓 = 𝐹 → (Base‘𝑓) = 𝐵) | 
| 8 | 7 | adantl 481 | . . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐵) | 
| 9 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) | 
| 10 |  | isassa.v | . . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) | 
| 11 | 9, 10 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) | 
| 12 |  | isassa.s | . . . . . . . . 9
⊢  · = (
·𝑠 ‘𝑊) | 
| 13 |  | isassa.t | . . . . . . . . 9
⊢  × =
(.r‘𝑊) | 
| 14 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → 𝑡 = × ) | 
| 15 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑠 = · ∧ 𝑡 = × ) → 𝑠 = · ) | 
| 16 | 15 | oveqd 7448 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥)) | 
| 17 |  | eqidd 2738 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → 𝑦 = 𝑦) | 
| 18 | 14, 16, 17 | oveq123d 7452 | . . . . . . . . . . 11
⊢ ((𝑠 = · ∧ 𝑡 = × ) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦)) | 
| 19 |  | eqidd 2738 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → 𝑟 = 𝑟) | 
| 20 | 14 | oveqd 7448 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (𝑥𝑡𝑦) = (𝑥 × 𝑦)) | 
| 21 | 15, 19, 20 | oveq123d 7452 | . . . . . . . . . . 11
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦))) | 
| 22 | 18, 21 | eqeq12d 2753 | . . . . . . . . . 10
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)))) | 
| 23 |  | eqidd 2738 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → 𝑥 = 𝑥) | 
| 24 | 15 | oveqd 7448 | . . . . . . . . . . . 12
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (𝑟𝑠𝑦) = (𝑟 · 𝑦)) | 
| 25 | 14, 23, 24 | oveq123d 7452 | . . . . . . . . . . 11
⊢ ((𝑠 = · ∧ 𝑡 = × ) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦))) | 
| 26 | 25, 21 | eqeq12d 2753 | . . . . . . . . . 10
⊢ ((𝑠 = · ∧ 𝑡 = × ) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) | 
| 27 | 22, 26 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝑠 = · ∧ 𝑡 = × ) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 28 | 12, 13, 27 | sbcie2s 17198 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ([(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 29 | 11, 28 | raleqbidv 3346 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 30 | 11, 29 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 31 | 30 | adantr 480 | . . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 32 | 8, 31 | raleqbidv 3346 | . . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 33 | 1, 4, 32 | sbcied2 3833 | . . 3
⊢ (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 34 |  | df-assa 21873 | . . 3
⊢ AssAlg =
{𝑤 ∈ (LMod ∩ Ring)
∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[(
·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))} | 
| 35 | 33, 34 | elrab2 3695 | . 2
⊢ (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 36 |  | elin 3967 | . . 3
⊢ (𝑊 ∈ (LMod ∩ Ring) ↔
(𝑊 ∈ LMod ∧ 𝑊 ∈ Ring)) | 
| 37 | 36 | anbi1i 624 | . 2
⊢ ((𝑊 ∈ (LMod ∩ Ring) ∧
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | 
| 38 | 35, 37 | bitri 275 | 1
⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧
∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) |