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

Theorem isassa 21876
Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
Hypotheses
Ref Expression
isassa.v 𝑉 = (Base‘𝑊)
isassa.f 𝐹 = (Scalar‘𝑊)
isassa.b 𝐵 = (Base‘𝐹)
isassa.s · = ( ·𝑠𝑊)
isassa.t × = (.r𝑊)
Assertion
Ref Expression
isassa (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
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 6921 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V)
2 fveq2 6906 . . . . 5 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
3 isassa.f . . . . 5 𝐹 = (Scalar‘𝑊)
42, 3eqtr4di 2795 . . . 4 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
5 fveq2 6906 . . . . . . 7 (𝑓 = 𝐹 → (Base‘𝑓) = (Base‘𝐹))
6 isassa.b . . . . . . 7 𝐵 = (Base‘𝐹)
75, 6eqtr4di 2795 . . . . . 6 (𝑓 = 𝐹 → (Base‘𝑓) = 𝐵)
87adantl 481 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (Base‘𝑓) = 𝐵)
9 fveq2 6906 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
10 isassa.v . . . . . . . 8 𝑉 = (Base‘𝑊)
119, 10eqtr4di 2795 . . . . . . 7 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
12 isassa.s . . . . . . . . 9 · = ( ·𝑠𝑊)
13 isassa.t . . . . . . . . 9 × = (.r𝑊)
14 simpr 484 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → 𝑡 = × )
15 simpl 482 . . . . . . . . . . . . 13 ((𝑠 = ·𝑡 = × ) → 𝑠 = · )
1615oveqd 7448 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
17 eqidd 2738 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → 𝑦 = 𝑦)
1814, 16, 17oveq123d 7452 . . . . . . . . . . 11 ((𝑠 = ·𝑡 = × ) → ((𝑟𝑠𝑥)𝑡𝑦) = ((𝑟 · 𝑥) × 𝑦))
19 eqidd 2738 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → 𝑟 = 𝑟)
2014oveqd 7448 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → (𝑥𝑡𝑦) = (𝑥 × 𝑦))
2115, 19, 20oveq123d 7452 . . . . . . . . . . 11 ((𝑠 = ·𝑡 = × ) → (𝑟𝑠(𝑥𝑡𝑦)) = (𝑟 · (𝑥 × 𝑦)))
2218, 21eqeq12d 2753 . . . . . . . . . 10 ((𝑠 = ·𝑡 = × ) → (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))))
23 eqidd 2738 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → 𝑥 = 𝑥)
2415oveqd 7448 . . . . . . . . . . . 12 ((𝑠 = ·𝑡 = × ) → (𝑟𝑠𝑦) = (𝑟 · 𝑦))
2514, 23, 24oveq123d 7452 . . . . . . . . . . 11 ((𝑠 = ·𝑡 = × ) → (𝑥𝑡(𝑟𝑠𝑦)) = (𝑥 × (𝑟 · 𝑦)))
2625, 21eqeq12d 2753 . . . . . . . . . 10 ((𝑠 = ·𝑡 = × ) → ((𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)) ↔ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
2722, 26anbi12d 632 . . . . . . . . 9 ((𝑠 = ·𝑡 = × ) → ((((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
2812, 13, 27sbcie2s 17198 . . . . . . . 8 (𝑤 = 𝑊 → ([( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
2911, 28raleqbidv 3346 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3011, 29raleqbidv 3346 . . . . . 6 (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3130adantr 480 . . . . 5 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
328, 31raleqbidv 3346 . . . 4 ((𝑤 = 𝑊𝑓 = 𝐹) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
331, 4, 32sbcied2 3833 . . 3 (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓]𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))) ↔ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
34 df-assa 21873 . . 3 AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓]𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))}
3533, 34elrab2 3695 . 2 (𝑊 ∈ AssAlg ↔ (𝑊 ∈ (LMod ∩ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
36 elin 3967 . . 3 (𝑊 ∈ (LMod ∩ Ring) ↔ (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
3736anbi1i 624 . 2 ((𝑊 ∈ (LMod ∩ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))) ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
3835, 37bitri 275 1 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  [wsbc 3788  cin 3950  cfv 6561  (class class class)co 7431  Basecbs 17247  .rcmulr 17298  Scalarcsca 17300   ·𝑠 cvsca 17301  Ringcrg 20230  LModclmod 20858  AssAlgcasa 21870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-assa 21873
This theorem is referenced by:  assalem  21877  assalmod  21880  assaring  21881  isassad  21885  assapropd  21892
  Copyright terms: Public domain W3C validator