Metamath Proof Explorer

Theorem 0mhm

Description: The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses 0mhm.z 
|- .0. = ( 0g ` N )
0mhm.b 
|- B = ( Base ` M )
Assertion 0mhm 
|- ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) e. ( M MndHom N ) )

Proof

Step Hyp Ref Expression
1 0mhm.z 
 |-  .0. = ( 0g ` N )
2 0mhm.b 
 |-  B = ( Base ` M )
3 id 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> ( M e. Mnd /\ N e. Mnd ) )
4 eqid 
 |-  ( Base ` N ) = ( Base ` N )
5 4 1 mndidcl 
 |-  ( N e. Mnd -> .0. e. ( Base ` N ) )
6 5 adantl 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> .0. e. ( Base ` N ) )
7 fconst6g 
 |-  ( .0. e. ( Base ` N ) -> ( B X. { .0. } ) : B --> ( Base ` N ) )
8 6 7 syl 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) : B --> ( Base ` N ) )
9 simpr 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> N e. Mnd )
10 eqid 
 |-  ( +g ` N ) = ( +g ` N )
11 4 10 1 mndlid 
 |-  ( ( N e. Mnd /\ .0. e. ( Base ` N ) ) -> ( .0. ( +g ` N ) .0. ) = .0. )
12 11 eqcomd 
 |-  ( ( N e. Mnd /\ .0. e. ( Base ` N ) ) -> .0. = ( .0. ( +g ` N ) .0. ) )
13 9 5 12 syl2anc2 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> .0. = ( .0. ( +g ` N ) .0. ) )
14 13 adantr 
 |-  ( ( ( M e. Mnd /\ N e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> .0. = ( .0. ( +g ` N ) .0. ) )
15 eqid 
 |-  ( +g ` M ) = ( +g ` M )
16 2 15 mndcl 
 |-  ( ( M e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` M ) y ) e. B )
17 16 3expb 
 |-  ( ( M e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` M ) y ) e. B )
18 17 adantlr 
 |-  ( ( ( M e. Mnd /\ N e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` M ) y ) e. B )
19 1 fvexi 
 |-  .0. e. _V
20 19 fvconst2 
 |-  ( ( x ( +g ` M ) y ) e. B -> ( ( B X. { .0. } ) ` ( x ( +g ` M ) y ) ) = .0. )
21 18 20 syl 
 |-  ( ( ( M e. Mnd /\ N e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( ( B X. { .0. } ) ` ( x ( +g ` M ) y ) ) = .0. )
22 19 fvconst2 
 |-  ( x e. B -> ( ( B X. { .0. } ) ` x ) = .0. )
23 19 fvconst2 
 |-  ( y e. B -> ( ( B X. { .0. } ) ` y ) = .0. )
24 22 23 oveqan12d 
 |-  ( ( x e. B /\ y e. B ) -> ( ( ( B X. { .0. } ) ` x ) ( +g ` N ) ( ( B X. { .0. } ) ` y ) ) = ( .0. ( +g ` N ) .0. ) )
25 24 adantl 
 |-  ( ( ( 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. ) )
26 14 21 25 3eqtr4d 
 |-  ( ( ( 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 ) ) )
27 26 ralrimivva 
 |-  ( ( 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 ) ) )
28 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
29 2 28 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
30 29 adantr 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> ( 0g ` M ) e. B )
31 19 fvconst2 
 |-  ( ( 0g ` M ) e. B -> ( ( B X. { .0. } ) ` ( 0g ` M ) ) = .0. )
32 30 31 syl 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> ( ( B X. { .0. } ) ` ( 0g ` M ) ) = .0. )
33 8 27 32 3jca 
 |-  ( ( 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. ) )
34 2 4 15 10 28 1 ismhm 
 |-  ( ( 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. ) ) )
35 3 33 34 sylanbrc 
 |-  ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) e. ( M MndHom N ) )