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

Theorem isassad 21199
Description: Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.)
Hypotheses
Ref Expression
isassad.v (𝜑𝑉 = (Base‘𝑊))
isassad.f (𝜑𝐹 = (Scalar‘𝑊))
isassad.b (𝜑𝐵 = (Base‘𝐹))
isassad.s (𝜑· = ( ·𝑠𝑊))
isassad.t (𝜑× = (.r𝑊))
isassad.1 (𝜑𝑊 ∈ LMod)
isassad.2 (𝜑𝑊 ∈ Ring)
isassad.3 (𝜑𝐹 ∈ CRing)
isassad.4 ((𝜑 ∧ (𝑟𝐵𝑥𝑉𝑦𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)))
isassad.5 ((𝜑 ∧ (𝑟𝐵𝑥𝑉𝑦𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))
Assertion
Ref Expression
isassad (𝜑𝑊 ∈ AssAlg)
Distinct variable groups:   𝑥,𝑟,𝑦,𝐵   𝜑,𝑟,𝑥,𝑦   𝑥,𝑉,𝑦   𝑊,𝑟,𝑥,𝑦
Allowed substitution hints:   · (𝑥,𝑦,𝑟)   × (𝑥,𝑦,𝑟)   𝐹(𝑥,𝑦,𝑟)   𝑉(𝑟)

Proof of Theorem isassad
StepHypRef Expression
1 isassad.1 . . 3 (𝜑𝑊 ∈ LMod)
2 isassad.2 . . 3 (𝜑𝑊 ∈ Ring)
3 isassad.f . . . 4 (𝜑𝐹 = (Scalar‘𝑊))
4 isassad.3 . . . 4 (𝜑𝐹 ∈ CRing)
53, 4eqeltrrd 2840 . . 3 (𝜑 → (Scalar‘𝑊) ∈ CRing)
61, 2, 53jca 1129 . 2 (𝜑 → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing))
7 isassad.4 . . . . 5 ((𝜑 ∧ (𝑟𝐵𝑥𝑉𝑦𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)))
8 isassad.5 . . . . 5 ((𝜑 ∧ (𝑟𝐵𝑥𝑉𝑦𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))
97, 8jca 513 . . . 4 ((𝜑 ∧ (𝑟𝐵𝑥𝑉𝑦𝑉)) → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
109ralrimivvva 3199 . . 3 (𝜑 → ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
11 isassad.b . . . . 5 (𝜑𝐵 = (Base‘𝐹))
123fveq2d 6842 . . . . 5 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝑊)))
1311, 12eqtrd 2778 . . . 4 (𝜑𝐵 = (Base‘(Scalar‘𝑊)))
14 isassad.v . . . . 5 (𝜑𝑉 = (Base‘𝑊))
15 isassad.t . . . . . . . . 9 (𝜑× = (.r𝑊))
16 isassad.s . . . . . . . . . 10 (𝜑· = ( ·𝑠𝑊))
1716oveqd 7367 . . . . . . . . 9 (𝜑 → (𝑟 · 𝑥) = (𝑟( ·𝑠𝑊)𝑥))
18 eqidd 2739 . . . . . . . . 9 (𝜑𝑦 = 𝑦)
1915, 17, 18oveq123d 7371 . . . . . . . 8 (𝜑 → ((𝑟 · 𝑥) × 𝑦) = ((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦))
20 eqidd 2739 . . . . . . . . 9 (𝜑𝑟 = 𝑟)
2115oveqd 7367 . . . . . . . . 9 (𝜑 → (𝑥 × 𝑦) = (𝑥(.r𝑊)𝑦))
2216, 20, 21oveq123d 7371 . . . . . . . 8 (𝜑 → (𝑟 · (𝑥 × 𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))
2319, 22eqeq12d 2754 . . . . . . 7 (𝜑 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦))))
24 eqidd 2739 . . . . . . . . 9 (𝜑𝑥 = 𝑥)
2516oveqd 7367 . . . . . . . . 9 (𝜑 → (𝑟 · 𝑦) = (𝑟( ·𝑠𝑊)𝑦))
2615, 24, 25oveq123d 7371 . . . . . . . 8 (𝜑 → (𝑥 × (𝑟 · 𝑦)) = (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)))
2726, 22eqeq12d 2754 . . . . . . 7 (𝜑 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦))))
2823, 27anbi12d 632 . . . . . 6 (𝜑 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
2914, 28raleqbidv 3318 . . . . 5 (𝜑 → (∀𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
3014, 29raleqbidv 3318 . . . 4 (𝜑 → (∀𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
3113, 30raleqbidv 3318 . . 3 (𝜑 → (∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
3210, 31mpbid 231 . 2 (𝜑 → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦))))
33 eqid 2738 . . 3 (Base‘𝑊) = (Base‘𝑊)
34 eqid 2738 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
35 eqid 2738 . . 3 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
36 eqid 2738 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
37 eqid 2738 . . 3 (.r𝑊) = (.r𝑊)
3833, 34, 35, 36, 37isassa 21191 . 2 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing) ∧ ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑟( ·𝑠𝑊)𝑦)) = (𝑟( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
396, 32, 38sylanbrc 584 1 (𝜑𝑊 ∈ AssAlg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3063  cfv 6492  (class class class)co 7350  Basecbs 17019  .rcmulr 17070  Scalarcsca 17072   ·𝑠 cvsca 17073  Ringcrg 19894  CRingccrg 19895  LModclmod 20251  AssAlgcasa 21185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-nul 5262
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rab 3407  df-v 3446  df-sbc 3739  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-assa 21188
This theorem is referenced by:  issubassa3  21200  sraassa  21202  zlmassa  21234  psrassa  21311  matassa  21721  mendassa  41423
  Copyright terms: Public domain W3C validator