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 ffvelcdmd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐴 ) ∈ 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 ( 𝑅 ‘ 𝐴 ) ) )