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

Theorem rngdi 20099
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 2728 . . . 4 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
3 rngdi.p . . . 4 + = (+gโ€˜๐‘…)
4 rngdi.t . . . 4 ยท = (.rโ€˜๐‘…)
51, 2, 3, 4isrng 20093 . . 3 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))))
6 oveq1 7427 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘ + ๐‘)))
7 oveq1 7427 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
8 oveq1 7427 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
97, 8oveq12d 7438 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)))
106, 9eqeq12d 2744 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘))))
11 oveq1 7427 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž + ๐‘) = (๐‘‹ + ๐‘))
1211oveq1d 7435 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘) ยท ๐‘))
138oveq1d 7435 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))
1412, 13eqeq12d 2744 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))))
1510, 14anbi12d 631 . . . . . 6 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))))
16 oveq1 7427 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ + ๐‘) = (๐‘Œ + ๐‘))
1716oveq2d 7436 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
18 oveq2 7428 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘Œ))
1918oveq1d 7435 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
2017, 19eqeq12d 2744 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
21 oveq2 7428 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ + ๐‘) = (๐‘‹ + ๐‘Œ))
2221oveq1d 7435 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
23 oveq1 7427 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ ยท ๐‘) = (๐‘Œ ยท ๐‘))
2423oveq2d 7436 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
2522, 24eqeq12d 2744 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
2620, 25anbi12d 631 . . . . . 6 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
27 oveq2 7428 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ + ๐‘) = (๐‘Œ + ๐‘))
2827oveq2d 7436 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
29 oveq2 7428 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘))
3029oveq2d 7436 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3128, 30eqeq12d 2744 . . . . . . 7 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
32 oveq2 7428 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
33 oveq2 7428 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ ยท ๐‘) = (๐‘Œ ยท ๐‘))
3429, 33oveq12d 7438 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
3532, 34eqeq12d 2744 . . . . . . 7 (๐‘ = ๐‘ โ†’ (((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
3631, 35anbi12d 631 . . . . . 6 (๐‘ = ๐‘ โ†’ (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
3715, 26, 36rspc3v 3625 . . . . 5 ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
38 simpl 482 . . . . 5 (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3937, 38syl6com 37 . . . 4 (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
40393ad2ant3 1133 . . 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 1085   = wceq 1534   โˆˆ wcel 2099  โˆ€wral 3058  โ€˜cfv 6548  (class class class)co 7420  Basecbs 17179  +gcplusg 17232  .rcmulr 17233  Smgrpcsgrp 18677  Abelcabl 19735  mulGrpcmgp 20073  Rngcrng 20091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-rng 20092
This theorem is referenced by:  rngrz  20105  rngmneg2  20107  rngsubdi  20110  prdsrngd  20115  imasrng  20116  opprrng  20283  issubrng2  20494  cntzsubrng  20503  rnglidlrng  21141  rngqiprngghmlem3  21178  rngqiprngimfolem  21179  rngqiprngfulem5  21204
  Copyright terms: Public domain W3C validator