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	$⊢ Y = S ⨉_{𝑠} R$
	prdspjmhm.b	$⊢ B = {Base}_{Y}$
	prdspjmhm.i	$⊢ φ \to I \in V$
	prdspjmhm.s	$⊢ φ \to S \in X$
	prdspjmhm.r	$⊢ φ \to R : I ⟶ Mnd$
	prdspjmhm.a	$⊢ φ \to A \in I$
Assertion	prdspjmhm	$⊢ φ \to (x \in B ⟼ x (A)) \in (Y MndHom R (A))$

Proof

Step	Hyp	Ref	Expression
1		prdspjmhm.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdspjmhm.b	$⊢ B = {Base}_{Y}$
3		prdspjmhm.i	$⊢ φ \to I \in V$
4		prdspjmhm.s	$⊢ φ \to S \in X$
5		prdspjmhm.r	$⊢ φ \to R : I ⟶ Mnd$
6		prdspjmhm.a	$⊢ φ \to A \in I$
7	1 3 4 5	prdsmndd	$⊢ φ \to Y \in Mnd$
8	5 6	ffvelcdmd	$⊢ φ \to R (A) \in Mnd$
9	4	adantr	$⊢ (φ \land x \in B) \to S \in X$
10	3	adantr	$⊢ (φ \land x \in B) \to I \in V$
11	5	ffnd	$⊢ φ \to R Fn I$
12	11	adantr	$⊢ (φ \land x \in B) \to R Fn I$
13		simpr	$⊢ (φ \land x \in B) \to x \in B$
14	6	adantr	$⊢ (φ \land x \in B) \to A \in I$
15	1 2 9 10 12 13 14	prdsbasprj	$⊢ (φ \land x \in B) \to x (A) \in {Base}_{R (A)}$
16	15	fmpttd	$⊢ φ \to (x \in B ⟼ x (A)) : B ⟶ {Base}_{R (A)}$
17	4	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to S \in X$
18	3	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to I \in V$
19	11	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to R Fn I$
20		simprl	$⊢ (φ \land (y \in B \land z \in B)) \to y \in B$
21		simprr	$⊢ (φ \land (y \in B \land z \in B)) \to z \in B$
22		eqid	$⊢ +_{Y} = +_{Y}$
23	6	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to A \in I$
24	1 2 17 18 19 20 21 22 23	prdsplusgfval	$⊢ (φ \land (y \in B \land z \in B)) \to (y +_{Y} z) (A) = y (A) +_{R (A)} z (A)$
25	2 22	mndcl	$⊢ (Y \in Mnd \land y \in B \land z \in B) \to y +_{Y} z \in B$
26	25	3expb	$⊢ (Y \in Mnd \land (y \in B \land z \in B)) \to y +_{Y} z \in B$
27	7 26	sylan	$⊢ (φ \land (y \in B \land z \in B)) \to y +_{Y} z \in B$
28		fveq1	$⊢ x = y +_{Y} z \to x (A) = (y +_{Y} z) (A)$
29		eqid	$⊢ (x \in B ⟼ x (A)) = (x \in B ⟼ x (A))$
30		fvex	$⊢ (y +_{Y} z) (A) \in V$
31	28 29 30	fvmpt	$⊢ y +_{Y} z \in B \to (x \in B ⟼ x (A)) (y +_{Y} z) = (y +_{Y} z) (A)$
32	27 31	syl	$⊢ (φ \land (y \in B \land z \in B)) \to (x \in B ⟼ x (A)) (y +_{Y} z) = (y +_{Y} z) (A)$
33		fveq1	$⊢ x = y \to x (A) = y (A)$
34		fvex	$⊢ y (A) \in V$
35	33 29 34	fvmpt	$⊢ y \in B \to (x \in B ⟼ x (A)) (y) = y (A)$
36		fveq1	$⊢ x = z \to x (A) = z (A)$
37		fvex	$⊢ z (A) \in V$
38	36 29 37	fvmpt	$⊢ z \in B \to (x \in B ⟼ x (A)) (z) = z (A)$
39	35 38	oveqan12d	$⊢ (y \in B \land z \in B) \to (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z) = y (A) +_{R (A)} z (A)$
40	39	adantl	$⊢ (φ \land (y \in B \land z \in B)) \to (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z) = y (A) +_{R (A)} z (A)$
41	24 32 40	3eqtr4d	$⊢ (φ \land (y \in B \land z \in B)) \to (x \in B ⟼ x (A)) (y +_{Y} z) = (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z)$
42	41	ralrimivva	$⊢ φ \to \forall y \in B \forall z \in B (x \in B ⟼ x (A)) (y +_{Y} z) = (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z)$
43		eqid	$⊢ 0_{Y} = 0_{Y}$
44	2 43	mndidcl	$⊢ Y \in Mnd \to 0_{Y} \in B$
45		fveq1	$⊢ x = 0_{Y} \to x (A) = 0_{Y} (A)$
46		fvex	$⊢ 0_{Y} (A) \in V$
47	45 29 46	fvmpt	$⊢ 0_{Y} \in B \to (x \in B ⟼ x (A)) (0_{Y}) = 0_{Y} (A)$
48	7 44 47	3syl	$⊢ φ \to (x \in B ⟼ x (A)) (0_{Y}) = 0_{Y} (A)$
49	1 3 4 5	prds0g	$⊢ φ \to 0_{𝑔} \circ R = 0_{Y}$
50	49	fveq1d	$⊢ φ \to (0_{𝑔} \circ R) (A) = 0_{Y} (A)$
51		fvco3	$⊢ (R : I ⟶ Mnd \land A \in I) \to (0_{𝑔} \circ R) (A) = 0_{R (A)}$
52	5 6 51	syl2anc	$⊢ φ \to (0_{𝑔} \circ R) (A) = 0_{R (A)}$
53	48 50 52	3eqtr2d	$⊢ φ \to (x \in B ⟼ x (A)) (0_{Y}) = 0_{R (A)}$
54	16 42 53	3jca	$⊢ φ \to ((x \in B ⟼ x (A)) : B ⟶ {Base}_{R (A)} \land \forall y \in B \forall z \in B (x \in B ⟼ x (A)) (y +_{Y} z) = (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z) \land (x \in B ⟼ x (A)) (0_{Y}) = 0_{R (A)})$
55		eqid	$⊢ {Base}_{R (A)} = {Base}_{R (A)}$
56		eqid	$⊢ +_{R (A)} = +_{R (A)}$
57		eqid	$⊢ 0_{R (A)} = 0_{R (A)}$
58	2 55 22 56 43 57	ismhm	$⊢ (x \in B ⟼ x (A)) \in (Y MndHom R (A)) \leftrightarrow ((Y \in Mnd \land R (A) \in Mnd) \land ((x \in B ⟼ x (A)) : B ⟶ {Base}_{R (A)} \land \forall y \in B \forall z \in B (x \in B ⟼ x (A)) (y +_{Y} z) = (x \in B ⟼ x (A)) (y) +_{R (A)} (x \in B ⟼ x (A)) (z) \land (x \in B ⟼ x (A)) (0_{Y}) = 0_{R (A)}))$
59	7 8 54 58	syl21anbrc	$⊢ φ \to (x \in B ⟼ x (A)) \in (Y MndHom R (A))$

Metamath Proof Explorer

Theorem prdspjmhm

Proof