pwsdiagmhm

Description: Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015)

	Ref	Expression
Hypotheses	pwsdiagmhm.y	$⊢ Y = R ↑_{𝑠} I$
	pwsdiagmhm.b	$⊢ B = {Base}_{R}$
	pwsdiagmhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
Assertion	pwsdiagmhm	$⊢ (R \in Mnd \land I \in W) \to F \in (R MndHom Y)$

Proof

Step	Hyp	Ref	Expression
1		pwsdiagmhm.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsdiagmhm.b	$⊢ B = {Base}_{R}$
3		pwsdiagmhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
4		simpl	$⊢ (R \in Mnd \land I \in W) \to R \in Mnd$
5	1	pwsmnd	$⊢ (R \in Mnd \land I \in W) \to Y \in Mnd$
6	2	fvexi	$⊢ B \in V$
7	3	fdiagfn	$⊢ (B \in V \land I \in W) \to F : B ⟶ B^{I}$
8	6 7	mpan	$⊢ I \in W \to F : B ⟶ B^{I}$
9	8	adantl	$⊢ (R \in Mnd \land I \in W) \to F : B ⟶ B^{I}$
10	1 2	pwsbas	$⊢ (R \in Mnd \land I \in W) \to B^{I} = {Base}_{Y}$
11	10	feq3d	$⊢ (R \in Mnd \land I \in W) \to (F : B ⟶ B^{I} \leftrightarrow F : B ⟶ {Base}_{Y})$
12	9 11	mpbid	$⊢ (R \in Mnd \land I \in W) \to F : B ⟶ {Base}_{Y}$
13		simplr	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to I \in W$
14		eqid	$⊢ +_{R} = +_{R}$
15	2 14	mndcl	$⊢ (R \in Mnd \land a \in B \land b \in B) \to a +_{R} b \in B$
16	15	3expb	$⊢ (R \in Mnd \land (a \in B \land b \in B)) \to a +_{R} b \in B$
17	16	adantlr	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to a +_{R} b \in B$
18	3	fvdiagfn	$⊢ (I \in W \land a +_{R} b \in B) \to F (a +_{R} b) = I \times \{a +_{R} b\}$
19	13 17 18	syl2anc	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to F (a +_{R} b) = I \times \{a +_{R} b\}$
20	3	fvdiagfn	$⊢ (I \in W \land a \in B) \to F (a) = I \times \{a\}$
21	3	fvdiagfn	$⊢ (I \in W \land b \in B) \to F (b) = I \times \{b\}$
22	20 21	oveqan12d	$⊢ ((I \in W \land a \in B) \land (I \in W \land b \in B)) \to F (a) +_{Y} F (b) = (I \times \{a\}) +_{Y} (I \times \{b\})$
23	22	anandis	$⊢ (I \in W \land (a \in B \land b \in B)) \to F (a) +_{Y} F (b) = (I \times \{a\}) +_{Y} (I \times \{b\})$
24	23	adantll	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to F (a) +_{Y} F (b) = (I \times \{a\}) +_{Y} (I \times \{b\})$
25		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
26		simpll	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to R \in Mnd$
27	1 2 25	pwsdiagel	$⊢ ((R \in Mnd \land I \in W) \land a \in B) \to I \times \{a\} \in {Base}_{Y}$
28	27	adantrr	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to I \times \{a\} \in {Base}_{Y}$
29	1 2 25	pwsdiagel	$⊢ ((R \in Mnd \land I \in W) \land b \in B) \to I \times \{b\} \in {Base}_{Y}$
30	29	adantrl	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to I \times \{b\} \in {Base}_{Y}$
31		eqid	$⊢ +_{Y} = +_{Y}$
32	1 25 26 13 28 30 14 31	pwsplusgval	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to (I \times \{a\}) +_{Y} (I \times \{b\}) = (I \times \{a\}) {+_{R}}_{f} (I \times \{b\})$
33		id	$⊢ I \in W \to I \in W$
34		vex	$⊢ a \in V$
35	34	a1i	$⊢ I \in W \to a \in V$
36		vex	$⊢ b \in V$
37	36	a1i	$⊢ I \in W \to b \in V$
38	33 35 37	ofc12	$⊢ I \in W \to (I \times \{a\}) {+_{R}}_{f} (I \times \{b\}) = I \times \{a +_{R} b\}$
39	38	ad2antlr	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to (I \times \{a\}) {+_{R}}_{f} (I \times \{b\}) = I \times \{a +_{R} b\}$
40	24 32 39	3eqtrd	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to F (a) +_{Y} F (b) = I \times \{a +_{R} b\}$
41	19 40	eqtr4d	$⊢ ((R \in Mnd \land I \in W) \land (a \in B \land b \in B)) \to F (a +_{R} b) = F (a) +_{Y} F (b)$
42	41	ralrimivva	$⊢ (R \in Mnd \land I \in W) \to \forall a \in B \forall b \in B F (a +_{R} b) = F (a) +_{Y} F (b)$
43		simpr	$⊢ (R \in Mnd \land I \in W) \to I \in W$
44		eqid	$⊢ 0_{R} = 0_{R}$
45	2 44	mndidcl	$⊢ R \in Mnd \to 0_{R} \in B$
46	45	adantr	$⊢ (R \in Mnd \land I \in W) \to 0_{R} \in B$
47	3	fvdiagfn	$⊢ (I \in W \land 0_{R} \in B) \to F (0_{R}) = I \times \{0_{R}\}$
48	43 46 47	syl2anc	$⊢ (R \in Mnd \land I \in W) \to F (0_{R}) = I \times \{0_{R}\}$
49	1 44	pws0g	$⊢ (R \in Mnd \land I \in W) \to I \times \{0_{R}\} = 0_{Y}$
50	48 49	eqtrd	$⊢ (R \in Mnd \land I \in W) \to F (0_{R}) = 0_{Y}$
51	12 42 50	3jca	$⊢ (R \in Mnd \land I \in W) \to (F : B ⟶ {Base}_{Y} \land \forall a \in B \forall b \in B F (a +_{R} b) = F (a) +_{Y} F (b) \land F (0_{R}) = 0_{Y})$
52		eqid	$⊢ 0_{Y} = 0_{Y}$
53	2 25 14 31 44 52	ismhm	$⊢ F \in (R MndHom Y) \leftrightarrow ((R \in Mnd \land Y \in Mnd) \land (F : B ⟶ {Base}_{Y} \land \forall a \in B \forall b \in B F (a +_{R} b) = F (a) +_{Y} F (b) \land F (0_{R}) = 0_{Y}))$
54	4 5 51 53	syl21anbrc	$⊢ (R \in Mnd \land I \in W) \to F \in (R MndHom Y)$

Metamath Proof Explorer

Theorem pwsdiagmhm

Proof