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

Theorem isassa 21169
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 6845 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
2 fveq2 6830 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
3 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
42, 3eqtr4di 2795 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
5 simpr 486 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → 𝑓 = 𝐹)
65eleq1d 2822 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
75fveq2d 6834 . . . . . . 7 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
8 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
97, 8eqtr4di 2795 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
10 fveq2 6830 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
11 isassa.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
1210, 11eqtr4di 2795 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
13 fvexd 6845 . . . . . . . . . 10 (𝑤 = 𝑊 → ( ·𝑠𝑤) ∈ V)
14 fvexd 6845 . . . . . . . . . . 11 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → (.r𝑤) ∈ V)
15 simpr 486 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = (.r𝑤))
16 fveq2 6830 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → (.r𝑤) = (.r𝑊))
1716ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = (.r𝑊))
18 isassa.t . . . . . . . . . . . . . . . 16 × = (.r𝑊)
1917, 18eqtr4di 2795 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = × )
2015, 19eqtrd 2777 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = × )
21 simplr 767 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = ( ·𝑠𝑤))
22 fveq2 6830 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
2322ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = ( ·𝑠𝑊))
24 isassa.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
2523, 24eqtr4di 2795 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = · )
2621, 25eqtrd 2777 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = · )
2726oveqd 7359 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
28 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑦 = 𝑦)
2920, 27, 28oveq123d 7363 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
30 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑟 = 𝑟)
3120oveqd 7359 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
3226, 30, 31oveq123d 7363 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
3329, 32eqeq12d 2753 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
34 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑥 = 𝑥)
3526oveqd 7359 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
3620, 34, 35oveq123d 7363 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
3736, 32eqeq12d 2753 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
3833, 37anbi12d 632 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3914, 38sbcied 3776 . . . . . . . . . 10 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → ([(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4013, 39sbcied 3776 . . . . . . . . 9 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4112, 40raleqbidv 3316 . . . . . . . 8 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4212, 41raleqbidv 3316 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4342adantr 482 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
449, 43raleqbidv 3316 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
456, 44anbi12d 632 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → ((𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
461, 4, 45sbcied2 3778 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
47 df-assa 21166 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
4846, 47elrab2 3641 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
49 anass 470 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
50 elin 3918 . . . . 5 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
5150anbi1i 625 . . . 4 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
52 df-3an 1089 . . . 4 ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
5351, 52bitr4i 278 . . 3 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing))
5453anbi1i 625 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
5548, 49, 543bitr2i 299 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wral 3062  Vcvv 3442  [wsbc 3731  cin 3901  cfv 6484  (class class class)co 7342  Basecbs 17010  .rcmulr 17061  Scalarcsca 17063   ·𝑠 cvsca 17064  Ringcrg 19878  CRingccrg 19879  LModclmod 20229  AssAlgcasa 21163
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 2708  ax-nul 5255
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rab 3405  df-v 3444  df-sbc 3732  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-iota 6436  df-fv 6492  df-ov 7345  df-assa 21166
This theorem is referenced by:  assalem  21170  assalmod  21173  assaring  21174  assasca  21175  isassad  21177  assapropd  21182
  Copyright terms: Public domain W3C validator