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

Theorem isassa 19229
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 fvex 6160 . . . . 5 (Scalar‘𝑤) ∈ V
21a1i 11 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
3 fveq2 6150 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
4 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
53, 4syl6eqr 2678 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
6 simpr 477 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → 𝑓 = 𝐹)
76eleq1d 2688 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
86fveq2d 6154 . . . . . . 7 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
9 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
108, 9syl6eqr 2678 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
11 fveq2 6150 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
12 isassa.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
1311, 12syl6eqr 2678 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
14 fvex 6160 . . . . . . . . . . 11 ( ·𝑠𝑤) ∈ V
1514a1i 11 . . . . . . . . . 10 (𝑤 = 𝑊 → ( ·𝑠𝑤) ∈ V)
16 fvex 6160 . . . . . . . . . . . 12 (.r𝑤) ∈ V
1716a1i 11 . . . . . . . . . . 11 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → (.r𝑤) ∈ V)
18 simpr 477 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = (.r𝑤))
19 fveq2 6150 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → (.r𝑤) = (.r𝑊))
2019ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = (.r𝑊))
21 isassa.t . . . . . . . . . . . . . . . 16 × = (.r𝑊)
2220, 21syl6eqr 2678 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = × )
2318, 22eqtrd 2660 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = × )
24 simplr 791 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = ( ·𝑠𝑤))
25 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
2625ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = ( ·𝑠𝑊))
27 isassa.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
2826, 27syl6eqr 2678 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = · )
2924, 28eqtrd 2660 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = · )
3029oveqd 6622 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
31 eqidd 2627 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑦 = 𝑦)
3223, 30, 31oveq123d 6626 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
33 eqidd 2627 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑟 = 𝑟)
3423oveqd 6622 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
3529, 33, 34oveq123d 6626 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
3632, 35eqeq12d 2641 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
37 eqidd 2627 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑥 = 𝑥)
3829oveqd 6622 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
3923, 37, 38oveq123d 6626 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
4039, 35eqeq12d 2641 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
4136, 40anbi12d 746 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4217, 41sbcied 3459 . . . . . . . . . 10 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → ([(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4315, 42sbcied 3459 . . . . . . . . 9 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4413, 43raleqbidv 3146 . . . . . . . 8 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4513, 44raleqbidv 3146 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4645adantr 481 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4710, 46raleqbidv 3146 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
487, 47anbi12d 746 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → ((𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
492, 5, 48sbcied2 3460 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
50 df-assa 19226 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
5149, 50elrab2 3353 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
52 anass 680 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
53 elin 3779 . . . . 5 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
5453anbi1i 730 . . . 4 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
55 df-3an 1038 . . . 4 ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
5654, 55bitr4i 267 . . 3 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing))
5756anbi1i 730 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
5851, 52, 573bitr2i 288 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1992  wral 2912  Vcvv 3191  [wsbc 3422  cin 3559  cfv 5850  (class class class)co 6605  Basecbs 15776  .rcmulr 15858  Scalarcsca 15860   ·𝑠 cvsca 15861  Ringcrg 18463  CRingccrg 18464  LModclmod 18779  AssAlgcasa 19223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-assa 19226
This theorem is referenced by:  assalem  19230  assalmod  19233  assaring  19234  assasca  19235  isassad  19237  assapropd  19241
  Copyright terms: Public domain W3C validator