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

Theorem assalem 21396
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
assalem ((𝑊 ∈ AssAlg ∧ (𝐴𝐵𝑋𝑉𝑌𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))

Proof of Theorem assalem
Dummy variables 𝑥 𝑟 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isassa.v . . . 4 𝑉 = (Base‘𝑊)
2 isassa.f . . . 4 𝐹 = (Scalar‘𝑊)
3 isassa.b . . . 4 𝐵 = (Base‘𝐹)
4 isassa.s . . . 4 · = ( ·𝑠𝑊)
5 isassa.t . . . 4 × = (.r𝑊)
61, 2, 3, 4, 5isassa 21395 . . 3 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)))))
76simprbi 498 . 2 (𝑊 ∈ AssAlg → ∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))
8 oveq1 7411 . . . . . 6 (𝑟 = 𝐴 → (𝑟 · 𝑥) = (𝐴 · 𝑥))
98oveq1d 7419 . . . . 5 (𝑟 = 𝐴 → ((𝑟 · 𝑥) × 𝑦) = ((𝐴 · 𝑥) × 𝑦))
10 oveq1 7411 . . . . 5 (𝑟 = 𝐴 → (𝑟 · (𝑥 × 𝑦)) = (𝐴 · (𝑥 × 𝑦)))
119, 10eqeq12d 2749 . . . 4 (𝑟 = 𝐴 → (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦))))
12 oveq1 7411 . . . . . 6 (𝑟 = 𝐴 → (𝑟 · 𝑦) = (𝐴 · 𝑦))
1312oveq2d 7420 . . . . 5 (𝑟 = 𝐴 → (𝑥 × (𝑟 · 𝑦)) = (𝑥 × (𝐴 · 𝑦)))
1413, 10eqeq12d 2749 . . . 4 (𝑟 = 𝐴 → ((𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦)) ↔ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))))
1511, 14anbi12d 632 . . 3 (𝑟 = 𝐴 → ((((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)))))
16 oveq2 7412 . . . . . 6 (𝑥 = 𝑋 → (𝐴 · 𝑥) = (𝐴 · 𝑋))
1716oveq1d 7419 . . . . 5 (𝑥 = 𝑋 → ((𝐴 · 𝑥) × 𝑦) = ((𝐴 · 𝑋) × 𝑦))
18 oveq1 7411 . . . . . 6 (𝑥 = 𝑋 → (𝑥 × 𝑦) = (𝑋 × 𝑦))
1918oveq2d 7420 . . . . 5 (𝑥 = 𝑋 → (𝐴 · (𝑥 × 𝑦)) = (𝐴 · (𝑋 × 𝑦)))
2017, 19eqeq12d 2749 . . . 4 (𝑥 = 𝑋 → (((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦))))
21 oveq1 7411 . . . . 5 (𝑥 = 𝑋 → (𝑥 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑦)))
2221, 19eqeq12d 2749 . . . 4 (𝑥 = 𝑋 → ((𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))))
2320, 22anbi12d 632 . . 3 (𝑥 = 𝑋 → ((((𝐴 · 𝑥) × 𝑦) = (𝐴 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝐴 · 𝑦)) = (𝐴 · (𝑥 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)))))
24 oveq2 7412 . . . . 5 (𝑦 = 𝑌 → ((𝐴 · 𝑋) × 𝑦) = ((𝐴 · 𝑋) × 𝑌))
25 oveq2 7412 . . . . . 6 (𝑦 = 𝑌 → (𝑋 × 𝑦) = (𝑋 × 𝑌))
2625oveq2d 7420 . . . . 5 (𝑦 = 𝑌 → (𝐴 · (𝑋 × 𝑦)) = (𝐴 · (𝑋 × 𝑌)))
2724, 26eqeq12d 2749 . . . 4 (𝑦 = 𝑌 → (((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ↔ ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))))
28 oveq2 7412 . . . . . 6 (𝑦 = 𝑌 → (𝐴 · 𝑦) = (𝐴 · 𝑌))
2928oveq2d 7420 . . . . 5 (𝑦 = 𝑌 → (𝑋 × (𝐴 · 𝑦)) = (𝑋 × (𝐴 · 𝑌)))
3029, 26eqeq12d 2749 . . . 4 (𝑦 = 𝑌 → ((𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦)) ↔ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))
3127, 30anbi12d 632 . . 3 (𝑦 = 𝑌 → ((((𝐴 · 𝑋) × 𝑦) = (𝐴 · (𝑋 × 𝑦)) ∧ (𝑋 × (𝐴 · 𝑦)) = (𝐴 · (𝑋 × 𝑦))) ↔ (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))))
3215, 23, 31rspc3v 3626 . 2 ((𝐴𝐵𝑋𝑉𝑌𝑉) → (∀𝑟𝐵𝑥𝑉𝑦𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))))
337, 32mpan9 508 1 ((𝑊 ∈ AssAlg ∧ (𝐴𝐵𝑋𝑉𝑌𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  cfv 6540  (class class class)co 7404  Basecbs 17140  .rcmulr 17194  Scalarcsca 17196   ·𝑠 cvsca 17197  Ringcrg 20047  LModclmod 20459  AssAlgcasa 21389
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 2704  ax-nul 5305
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 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407  df-assa 21392
This theorem is referenced by:  assaass  21397  assaassr  21398
  Copyright terms: Public domain W3C validator