Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngdir Structured version   Visualization version   GIF version

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

Proof of Theorem rngdir
Dummy variables ๐‘Ž ๐‘ ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rngdi.b . . . 4 ๐ต = (Baseโ€˜๐‘…)
2 eqid 2733 . . . 4 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
3 rngdi.p . . . 4 + = (+gโ€˜๐‘…)
4 rngdi.t . . . 4 ยท = (.rโ€˜๐‘…)
51, 2, 3, 4isrng 46650 . . 3 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))))
6 oveq1 7416 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘ + ๐‘)))
7 oveq1 7416 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
8 oveq1 7416 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
97, 8oveq12d 7427 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)))
106, 9eqeq12d 2749 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘))))
11 oveq1 7416 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž + ๐‘) = (๐‘‹ + ๐‘))
1211oveq1d 7424 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘) ยท ๐‘))
138oveq1d 7424 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))
1412, 13eqeq12d 2749 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))))
1510, 14anbi12d 632 . . . . . 6 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))))
16 oveq1 7416 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ + ๐‘) = (๐‘Œ + ๐‘))
1716oveq2d 7425 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
18 oveq2 7417 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘Œ))
1918oveq1d 7424 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
2017, 19eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
21 oveq2 7417 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ + ๐‘) = (๐‘‹ + ๐‘Œ))
2221oveq1d 7424 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
23 oveq1 7416 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ ยท ๐‘) = (๐‘Œ ยท ๐‘))
2423oveq2d 7425 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
2522, 24eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
2620, 25anbi12d 632 . . . . . 6 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
27 oveq2 7417 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ + ๐‘) = (๐‘Œ + ๐‘))
2827oveq2d 7425 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
29 oveq2 7417 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘))
3029oveq2d 7425 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3128, 30eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
32 oveq2 7417 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
33 oveq2 7417 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ ยท ๐‘) = (๐‘Œ ยท ๐‘))
3429, 33oveq12d 7427 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
3532, 34eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘ โ†’ (((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
3631, 35anbi12d 632 . . . . . 6 (๐‘ = ๐‘ โ†’ (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
3715, 26, 36rspc3v 3628 . . . . 5 ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
38 simpr 486 . . . . 5 (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
3937, 38syl6com 37 . . . 4 (โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
40393ad2ant3 1136 . . 3 ((๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))) โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
415, 40sylbi 216 . 2 (๐‘… โˆˆ Rng โ†’ ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
4241imp 408 1 ((๐‘… โˆˆ Rng โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3062  โ€˜cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Smgrpcsgrp 18609  Abelcabl 19649  mulGrpcmgp 19987  Rngcrng 46648
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 5307
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 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-rng 46649
This theorem is referenced by:  rnglz  46664  rngmneg1  46666  rngsubdir  46671  opprrng  46674  prdsrngd  46677  imasrng  46678  issubrng2  46737  cntzsubrng  46746  rnglidlrng  46758
  Copyright terms: Public domain W3C validator