MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abvmul Unicode version

Theorem abvmul 15590
Description: An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.)
Hypotheses
Ref Expression
abvf.a  |-  A  =  (AbsVal `  R )
abvf.b  |-  B  =  ( Base `  R
)
abvmul.t  |-  .x.  =  ( .r `  R )
Assertion
Ref Expression
abvmul  |-  ( ( F  e.  A  /\  X  e.  B  /\  Y  e.  B )  ->  ( F `  ( X  .x.  Y ) )  =  ( ( F `
 X )  x.  ( F `  Y
) ) )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem abvmul
StepHypRef Expression
1 abvf.a . . . . . . . 8  |-  A  =  (AbsVal `  R )
21abvrcl 15582 . . . . . . 7  |-  ( F  e.  A  ->  R  e.  Ring )
3 abvf.b . . . . . . . 8  |-  B  =  ( Base `  R
)
4 eqid 2286 . . . . . . . 8  |-  ( +g  `  R )  =  ( +g  `  R )
5 abvmul.t . . . . . . . 8  |-  .x.  =  ( .r `  R )
6 eqid 2286 . . . . . . . 8  |-  ( 0g
`  R )  =  ( 0g `  R
)
71, 3, 4, 5, 6isabv 15580 . . . . . . 7  |-  ( R  e.  Ring  ->  ( F  e.  A  <->  ( F : B --> ( 0 [,) 
+oo )  /\  A. x  e.  B  (
( ( F `  x )  =  0  <-> 
x  =  ( 0g
`  R ) )  /\  A. y  e.  B  ( ( F `
 ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y )
)  /\  ( F `  ( x ( +g  `  R ) y ) )  <_  ( ( F `  x )  +  ( F `  y ) ) ) ) ) ) )
82, 7syl 17 . . . . . 6  |-  ( F  e.  A  ->  ( F  e.  A  <->  ( F : B --> ( 0 [,) 
+oo )  /\  A. x  e.  B  (
( ( F `  x )  =  0  <-> 
x  =  ( 0g
`  R ) )  /\  A. y  e.  B  ( ( F `
 ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y )
)  /\  ( F `  ( x ( +g  `  R ) y ) )  <_  ( ( F `  x )  +  ( F `  y ) ) ) ) ) ) )
98ibi 234 . . . . 5  |-  ( F  e.  A  ->  ( F : B --> ( 0 [,)  +oo )  /\  A. x  e.  B  (
( ( F `  x )  =  0  <-> 
x  =  ( 0g
`  R ) )  /\  A. y  e.  B  ( ( F `
 ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y )
)  /\  ( F `  ( x ( +g  `  R ) y ) )  <_  ( ( F `  x )  +  ( F `  y ) ) ) ) ) )
109simprd 451 . . . 4  |-  ( F  e.  A  ->  A. x  e.  B  ( (
( F `  x
)  =  0  <->  x  =  ( 0g `  R ) )  /\  A. y  e.  B  ( ( F `  (
x  .x.  y )
)  =  ( ( F `  x )  x.  ( F `  y ) )  /\  ( F `  ( x ( +g  `  R
) y ) )  <_  ( ( F `
 x )  +  ( F `  y
) ) ) ) )
11 simpl 445 . . . . . . 7  |-  ( ( ( F `  (
x  .x.  y )
)  =  ( ( F `  x )  x.  ( F `  y ) )  /\  ( F `  ( x ( +g  `  R
) y ) )  <_  ( ( F `
 x )  +  ( F `  y
) ) )  -> 
( F `  (
x  .x.  y )
)  =  ( ( F `  x )  x.  ( F `  y ) ) )
1211ralimi 2621 . . . . . 6  |-  ( A. y  e.  B  (
( F `  (
x  .x.  y )
)  =  ( ( F `  x )  x.  ( F `  y ) )  /\  ( F `  ( x ( +g  `  R
) y ) )  <_  ( ( F `
 x )  +  ( F `  y
) ) )  ->  A. y  e.  B  ( F `  ( x 
.x.  y ) )  =  ( ( F `
 x )  x.  ( F `  y
) ) )
1312adantl 454 . . . . 5  |-  ( ( ( ( F `  x )  =  0  <-> 
x  =  ( 0g
`  R ) )  /\  A. y  e.  B  ( ( F `
 ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y )
)  /\  ( F `  ( x ( +g  `  R ) y ) )  <_  ( ( F `  x )  +  ( F `  y ) ) ) )  ->  A. y  e.  B  ( F `  ( x  .x.  y
) )  =  ( ( F `  x
)  x.  ( F `
 y ) ) )
1413ralimi 2621 . . . 4  |-  ( A. x  e.  B  (
( ( F `  x )  =  0  <-> 
x  =  ( 0g
`  R ) )  /\  A. y  e.  B  ( ( F `
 ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y )
)  /\  ( F `  ( x ( +g  `  R ) y ) )  <_  ( ( F `  x )  +  ( F `  y ) ) ) )  ->  A. x  e.  B  A. y  e.  B  ( F `  ( x  .x.  y
) )  =  ( ( F `  x
)  x.  ( F `
 y ) ) )
1510, 14syl 17 . . 3  |-  ( F  e.  A  ->  A. x  e.  B  A. y  e.  B  ( F `  ( x  .x.  y
) )  =  ( ( F `  x
)  x.  ( F `
 y ) ) )
16 oveq1 5828 . . . . . 6  |-  ( x  =  X  ->  (
x  .x.  y )  =  ( X  .x.  y ) )
1716fveq2d 5491 . . . . 5  |-  ( x  =  X  ->  ( F `  ( x  .x.  y ) )  =  ( F `  ( X  .x.  y ) ) )
18 fveq2 5487 . . . . . 6  |-  ( x  =  X  ->  ( F `  x )  =  ( F `  X ) )
1918oveq1d 5836 . . . . 5  |-  ( x  =  X  ->  (
( F `  x
)  x.  ( F `
 y ) )  =  ( ( F `
 X )  x.  ( F `  y
) ) )
2017, 19eqeq12d 2300 . . . 4  |-  ( x  =  X  ->  (
( F `  (
x  .x.  y )
)  =  ( ( F `  x )  x.  ( F `  y ) )  <->  ( F `  ( X  .x.  y
) )  =  ( ( F `  X
)  x.  ( F `
 y ) ) ) )
21 oveq2 5829 . . . . . 6  |-  ( y  =  Y  ->  ( X  .x.  y )  =  ( X  .x.  Y
) )
2221fveq2d 5491 . . . . 5  |-  ( y  =  Y  ->  ( F `  ( X  .x.  y ) )  =  ( F `  ( X  .x.  Y ) ) )
23 fveq2 5487 . . . . . 6  |-  ( y  =  Y  ->  ( F `  y )  =  ( F `  Y ) )
2423oveq2d 5837 . . . . 5  |-  ( y  =  Y  ->  (
( F `  X
)  x.  ( F `
 y ) )  =  ( ( F `
 X )  x.  ( F `  Y
) ) )
2522, 24eqeq12d 2300 . . . 4  |-  ( y  =  Y  ->  (
( F `  ( X  .x.  y ) )  =  ( ( F `
 X )  x.  ( F `  y
) )  <->  ( F `  ( X  .x.  Y
) )  =  ( ( F `  X
)  x.  ( F `
 Y ) ) ) )
2620, 25rspc2v 2893 . . 3  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( A. x  e.  B  A. y  e.  B  ( F `  ( x  .x.  y ) )  =  ( ( F `  x )  x.  ( F `  y ) )  -> 
( F `  ( X  .x.  Y ) )  =  ( ( F `
 X )  x.  ( F `  Y
) ) ) )
2715, 26syl5com 28 . 2  |-  ( F  e.  A  ->  (
( X  e.  B  /\  Y  e.  B
)  ->  ( F `  ( X  .x.  Y
) )  =  ( ( F `  X
)  x.  ( F `
 Y ) ) ) )
28273impib 1151 1  |-  ( ( F  e.  A  /\  X  e.  B  /\  Y  e.  B )  ->  ( F `  ( X  .x.  Y ) )  =  ( ( F `
 X )  x.  ( F `  Y
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 936    = wceq 1625    e. wcel 1687   A.wral 2546   class class class wbr 4026   -->wf 5219   ` cfv 5223  (class class class)co 5821   0cc0 8734    + caddc 8737    x. cmul 8739    +oocpnf 8861    <_ cle 8865   [,)cico 10654   Basecbs 13144   +g cplusg 13204   .rcmulr 13205   0gc0g 13396   Ringcrg 15333  AbsValcabv 15577
This theorem is referenced by:  abv1z  15593  abvneg  15595  abvrec  15597  abvdiv  15598  abvdom  15599  abvres  15600  nmmul  18171  sranlm  18191  abvcxp  20760  qabvexp  20771  ostthlem2  20773  ostth2lem2  20779  ostth3  20783
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-sbc 2995  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-mpt 4082  df-id 4310  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-fv 5231  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-map 6771  df-abv 15578
  Copyright terms: Public domain W3C validator