Metamath Proof Explorer


Theorem prdspjmhm

Description: A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses prdspjmhm.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdspjmhm.b 𝐵 = ( Base ‘ 𝑌 )
prdspjmhm.i ( 𝜑𝐼𝑉 )
prdspjmhm.s ( 𝜑𝑆𝑋 )
prdspjmhm.r ( 𝜑𝑅 : 𝐼 ⟶ Mnd )
prdspjmhm.a ( 𝜑𝐴𝐼 )
Assertion prdspjmhm ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ∈ ( 𝑌 MndHom ( 𝑅𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 prdspjmhm.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdspjmhm.b 𝐵 = ( Base ‘ 𝑌 )
3 prdspjmhm.i ( 𝜑𝐼𝑉 )
4 prdspjmhm.s ( 𝜑𝑆𝑋 )
5 prdspjmhm.r ( 𝜑𝑅 : 𝐼 ⟶ Mnd )
6 prdspjmhm.a ( 𝜑𝐴𝐼 )
7 1 3 4 5 prdsmndd ( 𝜑𝑌 ∈ Mnd )
8 5 6 ffvelrnd ( 𝜑 → ( 𝑅𝐴 ) ∈ Mnd )
9 4 adantr ( ( 𝜑𝑥𝐵 ) → 𝑆𝑋 )
10 3 adantr ( ( 𝜑𝑥𝐵 ) → 𝐼𝑉 )
11 5 ffnd ( 𝜑𝑅 Fn 𝐼 )
12 11 adantr ( ( 𝜑𝑥𝐵 ) → 𝑅 Fn 𝐼 )
13 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
14 6 adantr ( ( 𝜑𝑥𝐵 ) → 𝐴𝐼 )
15 1 2 9 10 12 13 14 prdsbasprj ( ( 𝜑𝑥𝐵 ) → ( 𝑥𝐴 ) ∈ ( Base ‘ ( 𝑅𝐴 ) ) )
16 15 fmpttd ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅𝐴 ) ) )
17 4 adantr ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑆𝑋 )
18 3 adantr ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝐼𝑉 )
19 11 adantr ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑅 Fn 𝐼 )
20 simprl ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑦𝐵 )
21 simprr ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑧𝐵 )
22 eqid ( +g𝑌 ) = ( +g𝑌 )
23 6 adantr ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝐴𝐼 )
24 1 2 17 18 19 20 21 22 23 prdsplusgfval ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ‘ 𝐴 ) = ( ( 𝑦𝐴 ) ( +g ‘ ( 𝑅𝐴 ) ) ( 𝑧𝐴 ) ) )
25 2 22 mndcl ( ( 𝑌 ∈ Mnd ∧ 𝑦𝐵𝑧𝐵 ) → ( 𝑦 ( +g𝑌 ) 𝑧 ) ∈ 𝐵 )
26 25 3expb ( ( 𝑌 ∈ Mnd ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑦 ( +g𝑌 ) 𝑧 ) ∈ 𝐵 )
27 7 26 sylan ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑦 ( +g𝑌 ) 𝑧 ) ∈ 𝐵 )
28 fveq1 ( 𝑥 = ( 𝑦 ( +g𝑌 ) 𝑧 ) → ( 𝑥𝐴 ) = ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ‘ 𝐴 ) )
29 eqid ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) = ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) )
30 fvex ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ‘ 𝐴 ) ∈ V
31 28 29 30 fvmpt ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ∈ 𝐵 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ‘ 𝐴 ) )
32 27 31 syl ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( 𝑦 ( +g𝑌 ) 𝑧 ) ‘ 𝐴 ) )
33 fveq1 ( 𝑥 = 𝑦 → ( 𝑥𝐴 ) = ( 𝑦𝐴 ) )
34 fvex ( 𝑦𝐴 ) ∈ V
35 33 29 34 fvmpt ( 𝑦𝐵 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) = ( 𝑦𝐴 ) )
36 fveq1 ( 𝑥 = 𝑧 → ( 𝑥𝐴 ) = ( 𝑧𝐴 ) )
37 fvex ( 𝑧𝐴 ) ∈ V
38 36 29 37 fvmpt ( 𝑧𝐵 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) = ( 𝑧𝐴 ) )
39 35 38 oveqan12d ( ( 𝑦𝐵𝑧𝐵 ) → ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) = ( ( 𝑦𝐴 ) ( +g ‘ ( 𝑅𝐴 ) ) ( 𝑧𝐴 ) ) )
40 39 adantl ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) = ( ( 𝑦𝐴 ) ( +g ‘ ( 𝑅𝐴 ) ) ( 𝑧𝐴 ) ) )
41 24 32 40 3eqtr4d ( ( 𝜑 ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) )
42 41 ralrimivva ( 𝜑 → ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) )
43 eqid ( 0g𝑌 ) = ( 0g𝑌 )
44 2 43 mndidcl ( 𝑌 ∈ Mnd → ( 0g𝑌 ) ∈ 𝐵 )
45 fveq1 ( 𝑥 = ( 0g𝑌 ) → ( 𝑥𝐴 ) = ( ( 0g𝑌 ) ‘ 𝐴 ) )
46 fvex ( ( 0g𝑌 ) ‘ 𝐴 ) ∈ V
47 45 29 46 fvmpt ( ( 0g𝑌 ) ∈ 𝐵 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 0g𝑌 ) ) = ( ( 0g𝑌 ) ‘ 𝐴 ) )
48 7 44 47 3syl ( 𝜑 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 0g𝑌 ) ) = ( ( 0g𝑌 ) ‘ 𝐴 ) )
49 1 3 4 5 prds0g ( 𝜑 → ( 0g𝑅 ) = ( 0g𝑌 ) )
50 49 fveq1d ( 𝜑 → ( ( 0g𝑅 ) ‘ 𝐴 ) = ( ( 0g𝑌 ) ‘ 𝐴 ) )
51 fvco3 ( ( 𝑅 : 𝐼 ⟶ Mnd ∧ 𝐴𝐼 ) → ( ( 0g𝑅 ) ‘ 𝐴 ) = ( 0g ‘ ( 𝑅𝐴 ) ) )
52 5 6 51 syl2anc ( 𝜑 → ( ( 0g𝑅 ) ‘ 𝐴 ) = ( 0g ‘ ( 𝑅𝐴 ) ) )
53 48 50 52 3eqtr2d ( 𝜑 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 0g𝑌 ) ) = ( 0g ‘ ( 𝑅𝐴 ) ) )
54 16 42 53 3jca ( 𝜑 → ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅𝐴 ) ) ∧ ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 0g𝑌 ) ) = ( 0g ‘ ( 𝑅𝐴 ) ) ) )
55 eqid ( Base ‘ ( 𝑅𝐴 ) ) = ( Base ‘ ( 𝑅𝐴 ) )
56 eqid ( +g ‘ ( 𝑅𝐴 ) ) = ( +g ‘ ( 𝑅𝐴 ) )
57 eqid ( 0g ‘ ( 𝑅𝐴 ) ) = ( 0g ‘ ( 𝑅𝐴 ) )
58 2 55 22 56 43 57 ismhm ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ∈ ( 𝑌 MndHom ( 𝑅𝐴 ) ) ↔ ( ( 𝑌 ∈ Mnd ∧ ( 𝑅𝐴 ) ∈ Mnd ) ∧ ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅𝐴 ) ) ∧ ∀ 𝑦𝐵𝑧𝐵 ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 𝑦 ( +g𝑌 ) 𝑧 ) ) = ( ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅𝐴 ) ) ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ‘ ( 0g𝑌 ) ) = ( 0g ‘ ( 𝑅𝐴 ) ) ) ) )
59 7 8 54 58 syl21anbrc ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑥𝐴 ) ) ∈ ( 𝑌 MndHom ( 𝑅𝐴 ) ) )