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

Theorem isassa 20543
 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 6667 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
2 fveq2 6652 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
3 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
42, 3eqtr4di 2875 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
5 simpr 488 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → 𝑓 = 𝐹)
65eleq1d 2898 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
75fveq2d 6656 . . . . . . 7 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
8 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
97, 8eqtr4di 2875 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
10 fveq2 6652 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
11 isassa.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
1210, 11eqtr4di 2875 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
13 fvexd 6667 . . . . . . . . . 10 (𝑤 = 𝑊 → ( ·𝑠𝑤) ∈ V)
14 fvexd 6667 . . . . . . . . . . 11 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → (.r𝑤) ∈ V)
15 simpr 488 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = (.r𝑤))
16 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → (.r𝑤) = (.r𝑊))
1716ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = (.r𝑊))
18 isassa.t . . . . . . . . . . . . . . . 16 × = (.r𝑊)
1917, 18eqtr4di 2875 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = × )
2015, 19eqtrd 2857 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = × )
21 simplr 768 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = ( ·𝑠𝑤))
22 fveq2 6652 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
2322ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = ( ·𝑠𝑊))
24 isassa.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
2523, 24eqtr4di 2875 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = · )
2621, 25eqtrd 2857 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = · )
2726oveqd 7157 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
28 eqidd 2823 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑦 = 𝑦)
2920, 27, 28oveq123d 7161 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
30 eqidd 2823 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑟 = 𝑟)
3120oveqd 7157 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
3226, 30, 31oveq123d 7161 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
3329, 32eqeq12d 2838 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
34 eqidd 2823 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑥 = 𝑥)
3526oveqd 7157 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
3620, 34, 35oveq123d 7161 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
3736, 32eqeq12d 2838 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
3833, 37anbi12d 633 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3914, 38sbcied 3789 . . . . . . . . . 10 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → ([(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4013, 39sbcied 3789 . . . . . . . . 9 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4112, 40raleqbidv 3382 . . . . . . . 8 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4212, 41raleqbidv 3382 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4342adantr 484 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
449, 43raleqbidv 3382 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
456, 44anbi12d 633 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → ((𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
461, 4, 45sbcied2 3790 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
47 df-assa 20540 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
4846, 47elrab2 3658 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
49 anass 472 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
50 elin 3924 . . . . 5 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
5150anbi1i 626 . . . 4 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
52 df-3an 1086 . . . 4 ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
5351, 52bitr4i 281 . . 3 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing))
5453anbi1i 626 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
5548, 49, 543bitr2i 302 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114  ∀wral 3130  Vcvv 3469  [wsbc 3747   ∩ cin 3907  ‘cfv 6334  (class class class)co 7140  Basecbs 16474  .rcmulr 16557  Scalarcsca 16559   ·𝑠 cvsca 16560  Ringcrg 19288  CRingccrg 19289  LModclmod 19625  AssAlgcasa 20537 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-nul 5186 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143  df-assa 20540 This theorem is referenced by:  assalem  20544  assalmod  20547  assaring  20548  assasca  20549  isassad  20551  assapropd  20556
 Copyright terms: Public domain W3C validator