ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0mhm Unicode version

Theorem 0mhm 13058
Description: The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
0mhm.z  |-  .0.  =  ( 0g `  N )
0mhm.b  |-  B  =  ( Base `  M
)
Assertion
Ref Expression
0mhm  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( B  X.  {  .0.  } )  e.  ( M MndHom  N ) )

Proof of Theorem 0mhm
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 19 . 2  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( M  e.  Mnd  /\  N  e.  Mnd )
)
2 eqid 2193 . . . . . 6  |-  ( Base `  N )  =  (
Base `  N )
3 0mhm.z . . . . . 6  |-  .0.  =  ( 0g `  N )
42, 3mndidcl 13011 . . . . 5  |-  ( N  e.  Mnd  ->  .0.  e.  ( Base `  N
) )
54adantl 277 . . . 4  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  .0.  e.  ( Base `  N ) )
6 fconst6g 5452 . . . 4  |-  (  .0. 
e.  ( Base `  N
)  ->  ( B  X.  {  .0.  } ) : B --> ( Base `  N ) )
75, 6syl 14 . . 3  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( B  X.  {  .0.  } ) : B --> ( Base `  N )
)
8 simpr 110 . . . . . . 7  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  N  e.  Mnd )
9 eqid 2193 . . . . . . . . 9  |-  ( +g  `  N )  =  ( +g  `  N )
102, 9, 3mndlid 13016 . . . . . . . 8  |-  ( ( N  e.  Mnd  /\  .0.  e.  ( Base `  N
) )  ->  (  .0.  ( +g  `  N
)  .0.  )  =  .0.  )
1110eqcomd 2199 . . . . . . 7  |-  ( ( N  e.  Mnd  /\  .0.  e.  ( Base `  N
) )  ->  .0.  =  (  .0.  ( +g  `  N )  .0.  ) )
128, 4, 11syl2anc2 412 . . . . . 6  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  .0.  =  (  .0.  ( +g  `  N
)  .0.  ) )
1312adantr 276 . . . . 5  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  .0.  =  (  .0.  ( +g  `  N )  .0.  ) )
14 fn0g 12958 . . . . . . . . 9  |-  0g  Fn  _V
158elexd 2773 . . . . . . . . 9  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  N  e.  _V )
16 funfvex 5571 . . . . . . . . . 10  |-  ( ( Fun  0g  /\  N  e.  dom  0g )  -> 
( 0g `  N
)  e.  _V )
1716funfni 5354 . . . . . . . . 9  |-  ( ( 0g  Fn  _V  /\  N  e.  _V )  ->  ( 0g `  N
)  e.  _V )
1814, 15, 17sylancr 414 . . . . . . . 8  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( 0g `  N
)  e.  _V )
193, 18eqeltrid 2280 . . . . . . 7  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  .0.  e.  _V )
2019adantr 276 . . . . . 6  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  .0.  e.  _V )
21 0mhm.b . . . . . . . . 9  |-  B  =  ( Base `  M
)
22 eqid 2193 . . . . . . . . 9  |-  ( +g  `  M )  =  ( +g  `  M )
2321, 22mndcl 13004 . . . . . . . 8  |-  ( ( M  e.  Mnd  /\  x  e.  B  /\  y  e.  B )  ->  ( x ( +g  `  M ) y )  e.  B )
24233expb 1206 . . . . . . 7  |-  ( ( M  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x ( +g  `  M
) y )  e.  B )
2524adantlr 477 . . . . . 6  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x ( +g  `  M
) y )  e.  B )
26 fvconst2g 5772 . . . . . 6  |-  ( (  .0.  e.  _V  /\  ( x ( +g  `  M ) y )  e.  B )  -> 
( ( B  X.  {  .0.  } ) `  ( x ( +g  `  M ) y ) )  =  .0.  )
2720, 25, 26syl2anc 411 . . . . 5  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( B  X.  {  .0.  } ) `  (
x ( +g  `  M
) y ) )  =  .0.  )
28 simprl 529 . . . . . . 7  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  x  e.  B )
29 fvconst2g 5772 . . . . . . 7  |-  ( (  .0.  e.  _V  /\  x  e.  B )  ->  ( ( B  X.  {  .0.  } ) `  x )  =  .0.  )
3020, 28, 29syl2anc 411 . . . . . 6  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( B  X.  {  .0.  } ) `  x
)  =  .0.  )
31 simprr 531 . . . . . . 7  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  y  e.  B )
32 fvconst2g 5772 . . . . . . 7  |-  ( (  .0.  e.  _V  /\  y  e.  B )  ->  ( ( B  X.  {  .0.  } ) `  y )  =  .0.  )
3320, 31, 32syl2anc 411 . . . . . 6  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( B  X.  {  .0.  } ) `  y
)  =  .0.  )
3430, 33oveq12d 5936 . . . . 5  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( ( B  X.  {  .0.  } ) `  x ) ( +g  `  N ) ( ( B  X.  {  .0.  } ) `  y ) )  =  (  .0.  ( +g  `  N
)  .0.  ) )
3513, 27, 343eqtr4d 2236 . . . 4  |-  ( ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( B  X.  {  .0.  } ) `  (
x ( +g  `  M
) y ) )  =  ( ( ( B  X.  {  .0.  } ) `  x ) ( +g  `  N
) ( ( B  X.  {  .0.  }
) `  y )
) )
3635ralrimivva 2576 . . 3  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  A. x  e.  B  A. y  e.  B  ( ( B  X.  {  .0.  } ) `  ( x ( +g  `  M ) y ) )  =  ( ( ( B  X.  {  .0.  } ) `  x
) ( +g  `  N
) ( ( B  X.  {  .0.  }
) `  y )
) )
37 eqid 2193 . . . . . 6  |-  ( 0g
`  M )  =  ( 0g `  M
)
3821, 37mndidcl 13011 . . . . 5  |-  ( M  e.  Mnd  ->  ( 0g `  M )  e.  B )
3938adantr 276 . . . 4  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( 0g `  M
)  e.  B )
40 fvconst2g 5772 . . . 4  |-  ( (  .0.  e.  _V  /\  ( 0g `  M )  e.  B )  -> 
( ( B  X.  {  .0.  } ) `  ( 0g `  M ) )  =  .0.  )
4119, 39, 40syl2anc 411 . . 3  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( ( B  X.  {  .0.  } ) `  ( 0g `  M ) )  =  .0.  )
427, 36, 413jca 1179 . 2  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( ( B  X.  {  .0.  } ) : B --> ( Base `  N
)  /\  A. x  e.  B  A. y  e.  B  ( ( B  X.  {  .0.  }
) `  ( x
( +g  `  M ) y ) )  =  ( ( ( B  X.  {  .0.  }
) `  x )
( +g  `  N ) ( ( B  X.  {  .0.  } ) `  y ) )  /\  ( ( B  X.  {  .0.  } ) `  ( 0g `  M ) )  =  .0.  )
)
4321, 2, 22, 9, 37, 3ismhm 13033 . 2  |-  ( ( B  X.  {  .0.  } )  e.  ( M MndHom  N )  <->  ( ( M  e.  Mnd  /\  N  e.  Mnd )  /\  (
( B  X.  {  .0.  } ) : B --> ( Base `  N )  /\  A. x  e.  B  A. y  e.  B  ( ( B  X.  {  .0.  } ) `  ( x ( +g  `  M ) y ) )  =  ( ( ( B  X.  {  .0.  } ) `  x
) ( +g  `  N
) ( ( B  X.  {  .0.  }
) `  y )
)  /\  ( ( B  X.  {  .0.  }
) `  ( 0g `  M ) )  =  .0.  ) ) )
441, 42, 43sylanbrc 417 1  |-  ( ( M  e.  Mnd  /\  N  e.  Mnd )  ->  ( B  X.  {  .0.  } )  e.  ( M MndHom  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 980    = wceq 1364    e. wcel 2164   A.wral 2472   _Vcvv 2760   {csn 3618    X. cxp 4657    Fn wfn 5249   -->wf 5250   ` cfv 5254  (class class class)co 5918   Basecbs 12618   +g cplusg 12695   0gc0g 12867   Mndcmnd 12997   MndHom cmhm 13029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-map 6704  df-inn 8983  df-2 9041  df-ndx 12621  df-slot 12622  df-base 12624  df-plusg 12708  df-0g 12869  df-mgm 12939  df-sgrp 12985  df-mnd 12998  df-mhm 13031
This theorem is referenced by:  0ghm  13328
  Copyright terms: Public domain W3C validator