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

Theorem rngdi 20061
Description: Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.)
Hypotheses
Ref Expression
rngdi.b ๐ต = (Baseโ€˜๐‘…)
rngdi.p + = (+gโ€˜๐‘…)
rngdi.t ยท = (.rโ€˜๐‘…)
Assertion
Ref Expression
rngdi ((๐‘… โˆˆ Rng โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))

Proof of Theorem rngdi
Dummy variables ๐‘Ž ๐‘ ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rngdi.b . . . 4 ๐ต = (Baseโ€˜๐‘…)
2 eqid 2724 . . . 4 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
3 rngdi.p . . . 4 + = (+gโ€˜๐‘…)
4 rngdi.t . . . 4 ยท = (.rโ€˜๐‘…)
51, 2, 3, 4isrng 20055 . . 3 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))))
6 oveq1 7409 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘ + ๐‘)))
7 oveq1 7409 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
8 oveq1 7409 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
97, 8oveq12d 7420 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)))
106, 9eqeq12d 2740 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘))))
11 oveq1 7409 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž + ๐‘) = (๐‘‹ + ๐‘))
1211oveq1d 7417 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘) ยท ๐‘))
138oveq1d 7417 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))
1412, 13eqeq12d 2740 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))))
1510, 14anbi12d 630 . . . . . 6 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))))
16 oveq1 7409 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ + ๐‘) = (๐‘Œ + ๐‘))
1716oveq2d 7418 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
18 oveq2 7410 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘Œ))
1918oveq1d 7417 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
2017, 19eqeq12d 2740 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
21 oveq2 7410 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ + ๐‘) = (๐‘‹ + ๐‘Œ))
2221oveq1d 7417 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
23 oveq1 7409 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ ยท ๐‘) = (๐‘Œ ยท ๐‘))
2423oveq2d 7418 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
2522, 24eqeq12d 2740 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
2620, 25anbi12d 630 . . . . . 6 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
27 oveq2 7410 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ + ๐‘) = (๐‘Œ + ๐‘))
2827oveq2d 7418 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
29 oveq2 7410 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘))
3029oveq2d 7418 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3128, 30eqeq12d 2740 . . . . . . 7 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
32 oveq2 7410 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
33 oveq2 7410 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ ยท ๐‘) = (๐‘Œ ยท ๐‘))
3429, 33oveq12d 7420 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
3532, 34eqeq12d 2740 . . . . . . 7 (๐‘ = ๐‘ โ†’ (((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
3631, 35anbi12d 630 . . . . . 6 (๐‘ = ๐‘ โ†’ (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
3715, 26, 36rspc3v 3620 . . . . 5 ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
38 simpl 482 . . . . 5 (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3937, 38syl6com 37 . . . 4 (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
40393ad2ant3 1132 . . 3 ((๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))) โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
415, 40sylbi 216 . 2 (๐‘… โˆˆ Rng โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
4241imp 406 1 ((๐‘… โˆˆ Rng โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3053  โ€˜cfv 6534  (class class class)co 7402  Basecbs 17149  +gcplusg 17202  .rcmulr 17203  Smgrpcsgrp 18647  Abelcabl 19697  mulGrpcmgp 20035  Rngcrng 20053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5297
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rab 3425  df-v 3468  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405  df-rng 20054
This theorem is referenced by:  rngrz  20067  rngmneg2  20069  rngsubdi  20072  prdsrngd  20077  imasrng  20078  opprrng  20243  issubrng2  20454  cntzsubrng  20463  rnglidlrng  21101  rngqiprngghmlem3  21138  rngqiprngimfolem  21139  rngqiprngfulem5  21164
  Copyright terms: Public domain W3C validator