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

Theorem isassa 19136
 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 6113 . . . . 5 (Scalar‘𝑤) ∈ V
21a1i 11 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
3 fveq2 6103 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
4 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
53, 4syl6eqr 2662 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
6 simpr 476 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → 𝑓 = 𝐹)
76eleq1d 2672 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
86fveq2d 6107 . . . . . . 7 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
9 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
108, 9syl6eqr 2662 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
11 fveq2 6103 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
12 isassa.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
1311, 12syl6eqr 2662 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
14 fvex 6113 . . . . . . . . . . 11 ( ·𝑠𝑤) ∈ V
1514a1i 11 . . . . . . . . . 10 (𝑤 = 𝑊 → ( ·𝑠𝑤) ∈ V)
16 fvex 6113 . . . . . . . . . . . 12 (.r𝑤) ∈ V
1716a1i 11 . . . . . . . . . . 11 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → (.r𝑤) ∈ V)
18 simpr 476 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = (.r𝑤))
19 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → (.r𝑤) = (.r𝑊))
2019ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = (.r𝑊))
21 isassa.t . . . . . . . . . . . . . . . 16 × = (.r𝑊)
2220, 21syl6eqr 2662 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (.r𝑤) = × )
2318, 22eqtrd 2644 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑡 = × )
24 simplr 788 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = ( ·𝑠𝑤))
25 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
2625ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = ( ·𝑠𝑊))
27 isassa.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
2826, 27syl6eqr 2662 . . . . . . . . . . . . . . . 16 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ( ·𝑠𝑤) = · )
2924, 28eqtrd 2644 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑠 = · )
3029oveqd 6566 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
31 eqidd 2611 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑦 = 𝑦)
3223, 30, 31oveq123d 6570 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
33 eqidd 2611 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑟 = 𝑟)
3423oveqd 6566 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
3529, 33, 34oveq123d 6570 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
3632, 35eqeq12d 2625 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
37 eqidd 2611 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → 𝑥 = 𝑥)
3829oveqd 6566 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
3923, 37, 38oveq123d 6570 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
4039, 35eqeq12d 2625 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
4136, 40anbi12d 743 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) ∧ 𝑡 = (.r𝑤)) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4217, 41sbcied 3439 . . . . . . . . . 10 ((𝑤 = 𝑊𝑠 = ( ·𝑠𝑤)) → ([(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4315, 42sbcied 3439 . . . . . . . . 9 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4413, 43raleqbidv 3129 . . . . . . . 8 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4513, 44raleqbidv 3129 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4645adantr 480 . . . . . 6 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
4710, 46raleqbidv 3129 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
487, 47anbi12d 743 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → ((𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
492, 5, 48sbcied2 3440 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))) ↔ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
50 df-assa 19133 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
5149, 50elrab2 3333 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
52 anass 679 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))))
53 elin 3758 . . . . 5 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
5453anbi1i 727 . . . 4 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
55 df-3an 1033 . . . 4 ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ 𝐹 ∈ CRing))
5654, 55bitr4i 266 . . 3 ((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing))
5756anbi1i 727 . 2 (((𝑊 ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
5851, 52, 573bitr2i 287 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173  [wsbc 3402   ∩ cin 3539  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  .rcmulr 15769  Scalarcsca 15771   ·𝑠 cvsca 15772  Ringcrg 18370  CRingccrg 18371  LModclmod 18686  AssAlgcasa 19130 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-assa 19133 This theorem is referenced by:  assalem  19137  assalmod  19140  assaring  19141  assasca  19142  isassad  19144  assapropd  19148
 Copyright terms: Public domain W3C validator