MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isassa Structured version   Visualization version   GIF version

Theorem isassa 21262
Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
isassa.v 𝑉 = (Base‘𝑊)
isassa.f 𝐹 = (Scalar‘𝑊)
isassa.b 𝐵 = (Base‘𝐹)
isassa.s · = ( ·𝑠𝑊)
isassa.t × = (.r𝑊)
Assertion
Ref Expression
isassa (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
Distinct variable groups:   𝑥,𝑟,𝑦   𝐵,𝑟   𝐹,𝑟   𝑉,𝑟,𝑥,𝑦   · ,𝑟,𝑥,𝑦   × ,𝑟,𝑥,𝑦   𝑊,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem isassa
Dummy variables 𝑓 𝑤 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6857 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
2 fveq2 6842 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
3 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
42, 3eqtr4di 2794 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
5 simpr 485 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → 𝑓 = 𝐹)
65eleq1d 2822 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
75fveq2d 6846 . . . . . . 7 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
8 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
97, 8eqtr4di 2794 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
10 fveq2 6842 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
11 isassa.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
1210, 11eqtr4di 2794 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
13 fvexd 6857 . . . . . . . . . 10 (𝑤 = 𝑊 → ( ·𝑠𝑤) ∈ V)
14 fvexd 6857 . . . . . . . . . . 11 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → (.r𝑤) ∈ V)
15 simpr 485 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = (.r𝑤))
16 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → (.r𝑤) = (.r𝑊))
1716ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = (.r𝑊))
18 isassa.t . . . . . . . . . . . . . . . 16 × = (.r𝑊)
1917, 18eqtr4di 2794 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = × )
2015, 19eqtrd 2776 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = × )
21 simplr 767 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = ( ·𝑠𝑤))
22 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
2322ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = ( ·𝑠𝑊))
24 isassa.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
2523, 24eqtr4di 2794 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = · )
2621, 25eqtrd 2776 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = · )
2726oveqd 7374 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
28 eqidd 2737 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑦 = 𝑦)
2920, 27, 28oveq123d 7378 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
30 eqidd 2737 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑟 = 𝑟)
3120oveqd 7374 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
3226, 30, 31oveq123d 7378 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
3329, 32eqeq12d 2752 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
34 eqidd 2737 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑥 = 𝑥)
3526oveqd 7374 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
3620, 34, 35oveq123d 7378 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
3736, 32eqeq12d 2752 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
3833, 37anbi12d 631 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3914, 38sbcied 3784 . . . . . . . . . 10 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → ([(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4013, 39sbcied 3784 . . . . . . . . 9 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4112, 40raleqbidv 3319 . . . . . . . 8 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4212, 41raleqbidv 3319 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4342adantr 481 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
449, 43raleqbidv 3319 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
456, 44anbi12d 631 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → ((𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
461, 4, 45sbcied2 3786 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
47 df-assa 21259 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
4846, 47elrab2 3648 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
49 anass 469 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
50 elin 3926 . . . . 5 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
5150anbi1i 624 . . . 4 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
52 df-3an 1089 . . . 4 ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
5351, 52bitr4i 277 . . 3 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing))
5453anbi1i 624 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
5548, 49, 543bitr2i 298 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445  [wsbc 3739  cin 3909  cfv 6496  (class class class)co 7357  Basecbs 17083  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  Ringcrg 19964  CRingccrg 19965  LModclmod 20322  AssAlgcasa 21256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-assa 21259
This theorem is referenced by:  assalem  21263  assalmod  21266  assaring  21267  assasca  21268  isassad  21270  assapropd  21275
  Copyright terms: Public domain W3C validator