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 𝑁 ) )