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𝑁 )
0mhm.b 𝐵 = ( Base ‘ 𝑀 )
Assertion 0mhm ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 MndHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0mhm.z 0 = ( 0g𝑁 )
2 0mhm.b 𝐵 = ( Base ‘ 𝑀 )
3 id ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) )
4 eqid ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
5 4 1 mndidcl ( 𝑁 ∈ Mnd → 0 ∈ ( Base ‘ 𝑁 ) )
6 5 adantl ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → 0 ∈ ( Base ‘ 𝑁 ) )
7 fconst6g ( 0 ∈ ( Base ‘ 𝑁 ) → ( 𝐵 × { 0 } ) : 𝐵 ⟶ ( Base ‘ 𝑁 ) )
8 6 7 syl ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 𝐵 × { 0 } ) : 𝐵 ⟶ ( Base ‘ 𝑁 ) )
9 simpr ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → 𝑁 ∈ Mnd )
10 eqid ( +g𝑁 ) = ( +g𝑁 )
11 4 10 1 mndlid ( ( 𝑁 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑁 ) ) → ( 0 ( +g𝑁 ) 0 ) = 0 )
12 11 eqcomd ( ( 𝑁 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑁 ) ) → 0 = ( 0 ( +g𝑁 ) 0 ) )
13 9 5 12 syl2anc2 ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → 0 = ( 0 ( +g𝑁 ) 0 ) )
14 13 adantr ( ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 0 = ( 0 ( +g𝑁 ) 0 ) )
15 eqid ( +g𝑀 ) = ( +g𝑀 )
16 2 15 mndcl ( ( 𝑀 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝐵 )
17 16 3expb ( ( 𝑀 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝐵 )
18 17 adantlr ( ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝐵 )
19 1 fvexi 0 ∈ V
20 19 fvconst2 ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝐵 → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = 0 )
21 18 20 syl ( ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = 0 )
22 19 fvconst2 ( 𝑥𝐵 → ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) = 0 )
23 19 fvconst2 ( 𝑦𝐵 → ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) = 0 )
24 22 23 oveqan12d ( ( 𝑥𝐵𝑦𝐵 ) → ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) = ( 0 ( +g𝑁 ) 0 ) )
25 24 adantl ( ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) = ( 0 ( +g𝑁 ) 0 ) )
26 14 21 25 3eqtr4d ( ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) )
27 26 ralrimivva ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) )
28 eqid ( 0g𝑀 ) = ( 0g𝑀 )
29 2 28 mndidcl ( 𝑀 ∈ Mnd → ( 0g𝑀 ) ∈ 𝐵 )
30 29 adantr ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 0g𝑀 ) ∈ 𝐵 )
31 19 fvconst2 ( ( 0g𝑀 ) ∈ 𝐵 → ( ( 𝐵 × { 0 } ) ‘ ( 0g𝑀 ) ) = 0 )
32 30 31 syl ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( ( 𝐵 × { 0 } ) ‘ ( 0g𝑀 ) ) = 0 )
33 8 27 32 3jca ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( ( 𝐵 × { 0 } ) : 𝐵 ⟶ ( Base ‘ 𝑁 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) ∧ ( ( 𝐵 × { 0 } ) ‘ ( 0g𝑀 ) ) = 0 ) )
34 2 4 15 10 28 1 ismhm ( ( 𝐵 × { 0 } ) ∈ ( 𝑀 MndHom 𝑁 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( ( 𝐵 × { 0 } ) : 𝐵 ⟶ ( Base ‘ 𝑁 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( +g𝑀 ) 𝑦 ) ) = ( ( ( 𝐵 × { 0 } ) ‘ 𝑥 ) ( +g𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) ∧ ( ( 𝐵 × { 0 } ) ‘ ( 0g𝑀 ) ) = 0 ) ) )
35 3 33 34 sylanbrc ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 MndHom 𝑁 ) )