imasmnd

Description: The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasmnd.u	$⊢ φ \to U = F “_{𝑠} R$
	imasmnd.v	$⊢ φ \to V = {Base}_{R}$
	imasmnd.p	$⊢ \underset{˙}{+} = +_{R}$
	imasmnd.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasmnd.e	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
	imasmnd.r	$⊢ φ \to R \in Mnd$
	imasmnd.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	imasmnd	$⊢ φ \to (U \in Mnd \land F (\underset{˙}{0}) = 0_{U})$

Proof

Step	Hyp	Ref	Expression
1		imasmnd.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasmnd.v	$⊢ φ \to V = {Base}_{R}$
3		imasmnd.p	$⊢ \underset{˙}{+} = +_{R}$
4		imasmnd.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
5		imasmnd.e	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
6		imasmnd.r	$⊢ φ \to R \in Mnd$
7		imasmnd.z	$⊢ \underset{˙}{0} = 0_{R}$
8	6	3ad2ant1	$⊢ (φ \land x \in V \land y \in V) \to R \in Mnd$
9		simp2	$⊢ (φ \land x \in V \land y \in V) \to x \in V$
10	2	3ad2ant1	$⊢ (φ \land x \in V \land y \in V) \to V = {Base}_{R}$
11	9 10	eleqtrd	$⊢ (φ \land x \in V \land y \in V) \to x \in {Base}_{R}$
12		simp3	$⊢ (φ \land x \in V \land y \in V) \to y \in V$
13	12 10	eleqtrd	$⊢ (φ \land x \in V \land y \in V) \to y \in {Base}_{R}$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	14 3	mndcl	$⊢ (R \in Mnd \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{+} y \in {Base}_{R}$
16	8 11 13 15	syl3anc	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in {Base}_{R}$
17	16 10	eleqtrrd	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
18	6	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to R \in Mnd$
19	11	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in {Base}_{R}$
20	13	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \in {Base}_{R}$
21		simpr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in V$
22	2	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to V = {Base}_{R}$
23	21 22	eleqtrd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in {Base}_{R}$
24	14 3	mndass	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
25	18 19 20 23 24	syl13anc	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
26	25	fveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F ((x \underset{˙}{+} y) \underset{˙}{+} z) = F (x \underset{˙}{+} (y \underset{˙}{+} z))$
27	14 7	mndidcl	$⊢ R \in Mnd \to \underset{˙}{0} \in {Base}_{R}$
28	6 27	syl	$⊢ φ \to \underset{˙}{0} \in {Base}_{R}$
29	28 2	eleqtrrd	$⊢ φ \to \underset{˙}{0} \in V$
30	2	eleq2d	$⊢ φ \to (x \in V \leftrightarrow x \in {Base}_{R})$
31	30	biimpa	$⊢ (φ \land x \in V) \to x \in {Base}_{R}$
32	14 3 7	mndlid	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to \underset{˙}{0} \underset{˙}{+} x = x$
33	6 31 32	syl2an2r	$⊢ (φ \land x \in V) \to \underset{˙}{0} \underset{˙}{+} x = x$
34	33	fveq2d	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
35	14 3 7	mndrid	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to x \underset{˙}{+} \underset{˙}{0} = x$
36	6 31 35	syl2an2r	$⊢ (φ \land x \in V) \to x \underset{˙}{+} \underset{˙}{0} = x$
37	36	fveq2d	$⊢ (φ \land x \in V) \to F (x \underset{˙}{+} \underset{˙}{0}) = F (x)$
38	1 2 3 4 5 6 17 26 29 34 37	imasmnd2	$⊢ φ \to (U \in Mnd \land F (\underset{˙}{0}) = 0_{U})$

Metamath Proof Explorer

Theorem imasmnd

Proof