imasmnd2

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))$
	imasmnd2.r	$⊢ φ \to R \in W$
	imasmnd2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
	imasmnd2.2	$⊢ (φ \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))$
	imasmnd2.3	$⊢ φ \to \underset{˙}{0} \in V$
	imasmnd2.4	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
	imasmnd2.5	$⊢ (φ \land x \in V) \to F (x \underset{˙}{+} \underset{˙}{0}) = F (x)$
Assertion	imasmnd2	$⊢ φ \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		imasmnd2.r	$⊢ φ \to R \in W$
7		imasmnd2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
8		imasmnd2.2	$⊢ (φ \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))$
9		imasmnd2.3	$⊢ φ \to \underset{˙}{0} \in V$
10		imasmnd2.4	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
11		imasmnd2.5	$⊢ (φ \land x \in V) \to F (x \underset{˙}{+} \underset{˙}{0}) = F (x)$
12	1 2 4 6	imasbas	$⊢ φ \to B = {Base}_{U}$
13		eqidd	$⊢ φ \to +_{U} = +_{U}$
14		eqid	$⊢ +_{U} = +_{U}$
15	7	3expb	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
16	15	caovclg	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{+} q \in V$
17	4 5 1 2 6 3 14 16	imasaddf	$⊢ φ \to +_{U} : B \times B ⟶ B$
18		fovrn	$⊢ (+_{U} : B \times B ⟶ B \land u \in B \land v \in B) \to u +_{U} v \in B$
19	17 18	syl3an1	$⊢ (φ \land u \in B \land v \in B) \to u +_{U} v \in B$
20		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
21	4 20	syl	$⊢ φ \to ran F = B$
22	21	eleq2d	$⊢ φ \to (u \in ran F \leftrightarrow u \in B)$
23	21	eleq2d	$⊢ φ \to (v \in ran F \leftrightarrow v \in B)$
24	21	eleq2d	$⊢ φ \to (w \in ran F \leftrightarrow w \in B)$
25	22 23 24	3anbi123d	$⊢ φ \to ((u \in ran F \land v \in ran F \land w \in ran F) \leftrightarrow (u \in B \land v \in B \land w \in B))$
26		fofn	$⊢ F : V \underset{onto}{⟶} B \to F Fn V$
27	4 26	syl	$⊢ φ \to F Fn V$
28		fvelrnb	$⊢ F Fn V \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
29		fvelrnb	$⊢ F Fn V \to (v \in ran F \leftrightarrow \exists y \in V F (y) = v)$
30		fvelrnb	$⊢ F Fn V \to (w \in ran F \leftrightarrow \exists z \in V F (z) = w)$
31	28 29 30	3anbi123d	$⊢ F Fn V \to ((u \in ran F \land v \in ran F \land w \in ran F) \leftrightarrow (\exists x \in V F (x) = u \land \exists y \in V F (y) = v \land \exists z \in V F (z) = w))$
32	27 31	syl	$⊢ φ \to ((u \in ran F \land v \in ran F \land w \in ran F) \leftrightarrow (\exists x \in V F (x) = u \land \exists y \in V F (y) = v \land \exists z \in V F (z) = w))$
33	25 32	bitr3d	$⊢ φ \to ((u \in B \land v \in B \land w \in B) \leftrightarrow (\exists x \in V F (x) = u \land \exists y \in V F (y) = v \land \exists z \in V F (z) = w))$
34		3reeanv	$⊢ \exists x \in V \exists y \in V \exists z \in V (F (x) = u \land F (y) = v \land F (z) = w) \leftrightarrow (\exists x \in V F (x) = u \land \exists y \in V F (y) = v \land \exists z \in V F (z) = w)$
35	33 34	syl6bbr	$⊢ φ \to ((u \in B \land v \in B \land w \in B) \leftrightarrow \exists x \in V \exists y \in V \exists z \in V (F (x) = u \land F (y) = v \land F (z) = w))$
36		simpl	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to φ$
37	7	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} y \in V$
38		simpr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in V$
39	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land x \underset{˙}{+} y \in V \land z \in V) \to F (x \underset{˙}{+} y) +_{U} F (z) = F ((x \underset{˙}{+} y) \underset{˙}{+} z)$
40	36 37 38 39	syl3anc	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x \underset{˙}{+} y) +_{U} F (z) = F ((x \underset{˙}{+} y) \underset{˙}{+} z)$
41		simpr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in V$
42	16	caovclg	$⊢ (φ \land (y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
43	42	3adantr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
44	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land x \in V \land y \underset{˙}{+} z \in V) \to F (x) +_{U} F (y \underset{˙}{+} z) = F (x \underset{˙}{+} (y \underset{˙}{+} z))$
45	36 41 43 44	syl3anc	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y \underset{˙}{+} z) = F (x \underset{˙}{+} (y \underset{˙}{+} z))$
46	8 40 45	3eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x \underset{˙}{+} y) +_{U} F (z) = F (x) +_{U} F (y \underset{˙}{+} z)$
47	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land x \in V \land y \in V) \to F (x) +_{U} F (y) = F (x \underset{˙}{+} y)$
48	47	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y) = F (x \underset{˙}{+} y)$
49	48	oveq1d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (F (x) +_{U} F (y)) +_{U} F (z) = F (x \underset{˙}{+} y) +_{U} F (z)$
50	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land y \in V \land z \in V) \to F (y) +_{U} F (z) = F (y \underset{˙}{+} z)$
51	50	3adant3r1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (y) +_{U} F (z) = F (y \underset{˙}{+} z)$
52	51	oveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} (F (y) +_{U} F (z)) = F (x) +_{U} F (y \underset{˙}{+} z)$
53	46 49 52	3eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (F (x) +_{U} F (y)) +_{U} F (z) = F (x) +_{U} (F (y) +_{U} F (z))$
54		simp1	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) = u$
55		simp2	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) = v$
56	54 55	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) +_{U} F (y) = u +_{U} v$
57		simp3	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (z) = w$
58	56 57	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to (F (x) +_{U} F (y)) +_{U} F (z) = (u +_{U} v) +_{U} w$
59	55 57	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) +_{U} F (z) = v +_{U} w$
60	54 59	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) +_{U} (F (y) +_{U} F (z)) = u +_{U} (v +_{U} w)$
61	58 60	eqeq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to ((F (x) +_{U} F (y)) +_{U} F (z) = F (x) +_{U} (F (y) +_{U} F (z)) \leftrightarrow (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
62	53 61	syl5ibcom	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to ((F (x) = u \land F (y) = v \land F (z) = w) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
63	62	3exp2	$⊢ φ \to (x \in V \to (y \in V \to (z \in V \to ((F (x) = u \land F (y) = v \land F (z) = w) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w)))))$
64	63	imp32	$⊢ (φ \land (x \in V \land y \in V)) \to (z \in V \to ((F (x) = u \land F (y) = v \land F (z) = w) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w)))$
65	64	rexlimdv	$⊢ (φ \land (x \in V \land y \in V)) \to (\exists z \in V (F (x) = u \land F (y) = v \land F (z) = w) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
66	65	rexlimdvva	$⊢ φ \to (\exists x \in V \exists y \in V \exists z \in V (F (x) = u \land F (y) = v \land F (z) = w) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
67	35 66	sylbid	$⊢ φ \to ((u \in B \land v \in B \land w \in B) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
68	67	imp	$⊢ (φ \land (u \in B \land v \in B \land w \in B)) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w)$
69		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
70	4 69	syl	$⊢ φ \to F : V ⟶ B$
71	70 9	ffvelrnd	$⊢ φ \to F (\underset{˙}{0}) \in B$
72	27 28	syl	$⊢ φ \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
73	22 72	bitr3d	$⊢ φ \to (u \in B \leftrightarrow \exists x \in V F (x) = u)$
74		simpl	$⊢ (φ \land x \in V) \to φ$
75	9	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{0} \in V$
76		simpr	$⊢ (φ \land x \in V) \to x \in V$
77	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land \underset{˙}{0} \in V \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0} \underset{˙}{+} x)$
78	74 75 76 77	syl3anc	$⊢ (φ \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0} \underset{˙}{+} x)$
79	78 10	eqtrd	$⊢ (φ \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (x)$
80		oveq2	$⊢ F (x) = u \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0}) +_{U} u$
81		id	$⊢ F (x) = u \to F (x) = u$
82	80 81	eqeq12d	$⊢ F (x) = u \to (F (\underset{˙}{0}) +_{U} F (x) = F (x) \leftrightarrow F (\underset{˙}{0}) +_{U} u = u)$
83	79 82	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to F (\underset{˙}{0}) +_{U} u = u)$
84	83	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to F (\underset{˙}{0}) +_{U} u = u)$
85	73 84	sylbid	$⊢ φ \to (u \in B \to F (\underset{˙}{0}) +_{U} u = u)$
86	85	imp	$⊢ (φ \land u \in B) \to F (\underset{˙}{0}) +_{U} u = u$
87	4 5 1 2 6 3 14	imasaddval	$⊢ (φ \land x \in V \land \underset{˙}{0} \in V) \to F (x) +_{U} F (\underset{˙}{0}) = F (x \underset{˙}{+} \underset{˙}{0})$
88	75 87	mpd3an3	$⊢ (φ \land x \in V) \to F (x) +_{U} F (\underset{˙}{0}) = F (x \underset{˙}{+} \underset{˙}{0})$
89	88 11	eqtrd	$⊢ (φ \land x \in V) \to F (x) +_{U} F (\underset{˙}{0}) = F (x)$
90		oveq1	$⊢ F (x) = u \to F (x) +_{U} F (\underset{˙}{0}) = u +_{U} F (\underset{˙}{0})$
91	90 81	eqeq12d	$⊢ F (x) = u \to (F (x) +_{U} F (\underset{˙}{0}) = F (x) \leftrightarrow u +_{U} F (\underset{˙}{0}) = u)$
92	89 91	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to u +_{U} F (\underset{˙}{0}) = u)$
93	92	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to u +_{U} F (\underset{˙}{0}) = u)$
94	73 93	sylbid	$⊢ φ \to (u \in B \to u +_{U} F (\underset{˙}{0}) = u)$
95	94	imp	$⊢ (φ \land u \in B) \to u +_{U} F (\underset{˙}{0}) = u$
96	12 13 19 68 71 86 95	ismndd	$⊢ φ \to U \in Mnd$
97	12 13 71 86 95	grpidd	$⊢ φ \to F (\underset{˙}{0}) = 0_{U}$
98	96 97	jca	$⊢ φ \to (U \in Mnd \land F (\underset{˙}{0}) = 0_{U})$

Metamath Proof Explorer

Theorem imasmnd2

Proof