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 46266
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 46260 . . 3 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง (mulGrpโ€˜๐‘…) โˆˆ Smgrp โˆง โˆ€๐‘Ž โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)))))
6 oveq1 7365 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘ + ๐‘)))
7 oveq1 7365 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
8 oveq1 7365 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž ยท ๐‘) = (๐‘‹ ยท ๐‘))
97, 8oveq12d 7376 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)))
106, 9eqeq12d 2749 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘))))
11 oveq1 7365 . . . . . . . . 9 (๐‘Ž = ๐‘‹ โ†’ (๐‘Ž + ๐‘) = (๐‘‹ + ๐‘))
1211oveq1d 7373 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘) ยท ๐‘))
138oveq1d 7373 . . . . . . . 8 (๐‘Ž = ๐‘‹ โ†’ ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))
1412, 13eqeq12d 2749 . . . . . . 7 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))))
1510, 14anbi12d 632 . . . . . 6 (๐‘Ž = ๐‘‹ โ†’ (((๐‘Ž ยท (๐‘ + ๐‘)) = ((๐‘Ž ยท ๐‘) + (๐‘Ž ยท ๐‘)) โˆง ((๐‘Ž + ๐‘) ยท ๐‘) = ((๐‘Ž ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)))))
16 oveq1 7365 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ + ๐‘) = (๐‘Œ + ๐‘))
1716oveq2d 7374 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท (๐‘ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
18 oveq2 7366 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘Œ))
1918oveq1d 7373 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
2017, 19eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
21 oveq2 7366 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘‹ + ๐‘) = (๐‘‹ + ๐‘Œ))
2221oveq1d 7373 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
23 oveq1 7365 . . . . . . . . 9 (๐‘ = ๐‘Œ โ†’ (๐‘ ยท ๐‘) = (๐‘Œ ยท ๐‘))
2423oveq2d 7374 . . . . . . . 8 (๐‘ = ๐‘Œ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
2522, 24eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
2620, 25anbi12d 632 . . . . . 6 (๐‘ = ๐‘Œ โ†’ (((๐‘‹ ยท (๐‘ + ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
27 oveq2 7366 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ + ๐‘) = (๐‘Œ + ๐‘))
2827oveq2d 7374 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท (๐‘Œ + ๐‘)) = (๐‘‹ ยท (๐‘Œ + ๐‘)))
29 oveq2 7366 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘‹ ยท ๐‘) = (๐‘‹ ยท ๐‘))
3029oveq2d 7374 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)))
3128, 30eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โ†” (๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘))))
32 oveq2 7366 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ + ๐‘Œ) ยท ๐‘))
33 oveq2 7366 . . . . . . . . 9 (๐‘ = ๐‘ โ†’ (๐‘Œ ยท ๐‘) = (๐‘Œ ยท ๐‘))
3429, 33oveq12d 7376 . . . . . . . 8 (๐‘ = ๐‘ โ†’ ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))
3532, 34eqeq12d 2749 . . . . . . 7 (๐‘ = ๐‘ โ†’ (((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)) โ†” ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))))
3631, 35anbi12d 632 . . . . . 6 (๐‘ = ๐‘ โ†’ (((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘))) โ†” ((๐‘‹ ยท (๐‘Œ + ๐‘)) = ((๐‘‹ ยท ๐‘Œ) + (๐‘‹ ยท ๐‘)) โˆง ((๐‘‹ + ๐‘Œ) ยท ๐‘) = ((๐‘‹ ยท ๐‘) + (๐‘Œ ยท ๐‘)))))
3715, 26, 36rspc3v 3592 . . . . 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 3061  โ€˜cfv 6497  (class class class)co 7358  Basecbs 17088  +gcplusg 17138  .rcmulr 17139  Smgrpcsgrp 18550  Abelcabl 19568  mulGrpcmgp 19901  Rngcrng 46258
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 5264
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 2941  df-ral 3062  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-rng 46259
This theorem is referenced by:  rnglz  46268
  Copyright terms: Public domain W3C validator