imasgrp2

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

	Ref	Expression
Hypotheses	imasgrp.u	$⊢ φ \to U = F “_{𝑠} R$
	imasgrp.v	$⊢ φ \to V = {Base}_{R}$
	imasgrp.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	imasgrp.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasgrp.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))$
	imasgrp2.r	$⊢ φ \to R \in W$
	imasgrp2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
	imasgrp2.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))$
	imasgrp2.3	$⊢ φ \to \underset{˙}{0} \in V$
	imasgrp2.4	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
	imasgrp2.5	$⊢ (φ \land x \in V) \to N \in V$
	imasgrp2.6	$⊢ (φ \land x \in V) \to F (N \underset{˙}{+} x) = F (\underset{˙}{0})$
Assertion	imasgrp2	$⊢ φ \to (U \in Grp \land F (\underset{˙}{0}) = 0_{U})$

Proof

Step	Hyp	Ref	Expression
1		imasgrp.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasgrp.v	$⊢ φ \to V = {Base}_{R}$
3		imasgrp.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
4		imasgrp.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
5		imasgrp.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		imasgrp2.r	$⊢ φ \to R \in W$
7		imasgrp2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
8		imasgrp2.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		imasgrp2.3	$⊢ φ \to \underset{˙}{0} \in V$
10		imasgrp2.4	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
11		imasgrp2.5	$⊢ (φ \land x \in V) \to N \in V$
12		imasgrp2.6	$⊢ (φ \land x \in V) \to F (N \underset{˙}{+} x) = F (\underset{˙}{0})$
13	1 2 4 6	imasbas	$⊢ φ \to B = {Base}_{U}$
14		eqidd	$⊢ φ \to +_{U} = +_{U}$
15	3	oveqd	$⊢ φ \to a \underset{˙}{+} b = a +_{R} b$
16	15	fveq2d	$⊢ φ \to F (a \underset{˙}{+} b) = F (a +_{R} b)$
17	3	oveqd	$⊢ φ \to p \underset{˙}{+} q = p +_{R} q$
18	17	fveq2d	$⊢ φ \to F (p \underset{˙}{+} q) = F (p +_{R} q)$
19	16 18	eqeq12d	$⊢ φ \to (F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q) \leftrightarrow F (a +_{R} b) = F (p +_{R} q))$
20	19	3ad2ant1	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q) \leftrightarrow F (a +_{R} b) = F (p +_{R} q))$
21	5 20	sylibd	$⊢ (φ \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 +_{R} b) = F (p +_{R} q))$
22		eqid	$⊢ +_{R} = +_{R}$
23		eqid	$⊢ +_{U} = +_{U}$
24	17	adantr	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{+} q = p +_{R} q$
25	7	3expb	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
26	25	caovclg	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{+} q \in V$
27	24 26	eqeltrrd	$⊢ (φ \land (p \in V \land q \in V)) \to p +_{R} q \in V$
28	4 21 1 2 6 22 23 27	imasaddf	$⊢ φ \to +_{U} : B \times B ⟶ B$
29		fovcdm	$⊢ (+_{U} : B \times B ⟶ B \land u \in B \land v \in B) \to u +_{U} v \in B$
30	28 29	syl3an1	$⊢ (φ \land u \in B \land v \in B) \to u +_{U} v \in B$
31		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
32	4 31	syl	$⊢ φ \to ran F = B$
33	32	eleq2d	$⊢ φ \to (u \in ran F \leftrightarrow u \in B)$
34	32	eleq2d	$⊢ φ \to (v \in ran F \leftrightarrow v \in B)$
35	32	eleq2d	$⊢ φ \to (w \in ran F \leftrightarrow w \in B)$
36	33 34 35	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))$
37		fofn	$⊢ F : V \underset{onto}{⟶} B \to F Fn V$
38	4 37	syl	$⊢ φ \to F Fn V$
39		fvelrnb	$⊢ F Fn V \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
40		fvelrnb	$⊢ F Fn V \to (v \in ran F \leftrightarrow \exists y \in V F (y) = v)$
41		fvelrnb	$⊢ F Fn V \to (w \in ran F \leftrightarrow \exists z \in V F (z) = w)$
42	39 40 41	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))$
43	38 42	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))$
44	36 43	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))$
45		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)$
46	44 45	bitr4di	$⊢ φ \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))$
47	3	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to \underset{˙}{+} = +_{R}$
48	47	oveqd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = (x \underset{˙}{+} y) +_{R} z$
49	48	fveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F ((x \underset{˙}{+} y) \underset{˙}{+} z) = F ((x \underset{˙}{+} y) +_{R} z)$
50	47	oveqd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} (y \underset{˙}{+} z) = x +_{R} (y \underset{˙}{+} z)$
51	50	fveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x \underset{˙}{+} (y \underset{˙}{+} z)) = F (x +_{R} (y \underset{˙}{+} z))$
52	8 49 51	3eqtr3d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F ((x \underset{˙}{+} y) +_{R} z) = F (x +_{R} (y \underset{˙}{+} z))$
53		simpl	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to φ$
54	7	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} y \in V$
55		simpr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in V$
56	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land x \underset{˙}{+} y \in V \land z \in V) \to F (x \underset{˙}{+} y) +_{U} F (z) = F ((x \underset{˙}{+} y) +_{R} z)$
57	53 54 55 56	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) +_{R} z)$
58		simpr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in V$
59	26	caovclg	$⊢ (φ \land (y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
60	59	3adantr1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{+} z \in V$
61	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land x \in V \land y \underset{˙}{+} z \in V) \to F (x) +_{U} F (y \underset{˙}{+} z) = F (x +_{R} (y \underset{˙}{+} z))$
62	53 58 60 61	syl3anc	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y \underset{˙}{+} z) = F (x +_{R} (y \underset{˙}{+} z))$
63	52 57 62	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)$
64	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land x \in V \land y \in V) \to F (x) +_{U} F (y) = F (x +_{R} y)$
65	64	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y) = F (x +_{R} y)$
66	47	oveqd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} y = x +_{R} y$
67	66	fveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x \underset{˙}{+} y) = F (x +_{R} y)$
68	65 67	eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (x) +_{U} F (y) = F (x \underset{˙}{+} y)$
69	68	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)$
70	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land y \in V \land z \in V) \to F (y) +_{U} F (z) = F (y +_{R} z)$
71	70	3adant3r1	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (y) +_{U} F (z) = F (y +_{R} z)$
72	47	oveqd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{+} z = y +_{R} z$
73	72	fveq2d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (y \underset{˙}{+} z) = F (y +_{R} z)$
74	71 73	eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to F (y) +_{U} F (z) = F (y \underset{˙}{+} z)$
75	74	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)$
76	63 69 75	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))$
77		simp1	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) = u$
78		simp2	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) = v$
79	77 78	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (x) +_{U} F (y) = u +_{U} v$
80		simp3	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (z) = w$
81	79 80	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$
82	78 80	oveq12d	$⊢ (F (x) = u \land F (y) = v \land F (z) = w) \to F (y) +_{U} F (z) = v +_{U} w$
83	77 82	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)$
84	81 83	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))$
85	76 84	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))$
86	85	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)))))$
87	86	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)))$
88	87	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))$
89	88	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))$
90	46 89	sylbid	$⊢ φ \to ((u \in B \land v \in B \land w \in B) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w))$
91	90	imp	$⊢ (φ \land (u \in B \land v \in B \land w \in B)) \to (u +_{U} v) +_{U} w = u +_{U} (v +_{U} w)$
92		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
93	4 92	syl	$⊢ φ \to F : V ⟶ B$
94	93 9	ffvelcdmd	$⊢ φ \to F (\underset{˙}{0}) \in B$
95	38 39	syl	$⊢ φ \to (u \in ran F \leftrightarrow \exists x \in V F (x) = u)$
96	33 95	bitr3d	$⊢ φ \to (u \in B \leftrightarrow \exists x \in V F (x) = u)$
97		simpl	$⊢ (φ \land x \in V) \to φ$
98	9	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{0} \in V$
99		simpr	$⊢ (φ \land x \in V) \to x \in V$
100	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land \underset{˙}{0} \in V \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0} +_{R} x)$
101	97 98 99 100	syl3anc	$⊢ (φ \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0} +_{R} x)$
102	3	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{+} = +_{R}$
103	102	oveqd	$⊢ (φ \land x \in V) \to \underset{˙}{0} \underset{˙}{+} x = \underset{˙}{0} +_{R} x$
104	103	fveq2d	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (\underset{˙}{0} +_{R} x)$
105	101 104 10	3eqtr2d	$⊢ (φ \land x \in V) \to F (\underset{˙}{0}) +_{U} F (x) = F (x)$
106		oveq2	$⊢ F (x) = u \to F (\underset{˙}{0}) +_{U} F (x) = F (\underset{˙}{0}) +_{U} u$
107		id	$⊢ F (x) = u \to F (x) = u$
108	106 107	eqeq12d	$⊢ F (x) = u \to (F (\underset{˙}{0}) +_{U} F (x) = F (x) \leftrightarrow F (\underset{˙}{0}) +_{U} u = u)$
109	105 108	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to F (\underset{˙}{0}) +_{U} u = u)$
110	109	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to F (\underset{˙}{0}) +_{U} u = u)$
111	96 110	sylbid	$⊢ φ \to (u \in B \to F (\underset{˙}{0}) +_{U} u = u)$
112	111	imp	$⊢ (φ \land u \in B) \to F (\underset{˙}{0}) +_{U} u = u$
113	93	adantr	$⊢ (φ \land x \in V) \to F : V ⟶ B$
114	113 11	ffvelcdmd	$⊢ (φ \land x \in V) \to F (N) \in B$
115	4 21 1 2 6 22 23	imasaddval	$⊢ (φ \land N \in V \land x \in V) \to F (N) +_{U} F (x) = F (N +_{R} x)$
116	97 11 99 115	syl3anc	$⊢ (φ \land x \in V) \to F (N) +_{U} F (x) = F (N +_{R} x)$
117	102	oveqd	$⊢ (φ \land x \in V) \to N \underset{˙}{+} x = N +_{R} x$
118	117	fveq2d	$⊢ (φ \land x \in V) \to F (N \underset{˙}{+} x) = F (N +_{R} x)$
119	116 118 12	3eqtr2d	$⊢ (φ \land x \in V) \to F (N) +_{U} F (x) = F (\underset{˙}{0})$
120		oveq1	$⊢ v = F (N) \to v +_{U} F (x) = F (N) +_{U} F (x)$
121	120	eqeq1d	$⊢ v = F (N) \to (v +_{U} F (x) = F (\underset{˙}{0}) \leftrightarrow F (N) +_{U} F (x) = F (\underset{˙}{0}))$
122	121	rspcev	$⊢ (F (N) \in B \land F (N) +_{U} F (x) = F (\underset{˙}{0})) \to \exists v \in B v +_{U} F (x) = F (\underset{˙}{0})$
123	114 119 122	syl2anc	$⊢ (φ \land x \in V) \to \exists v \in B v +_{U} F (x) = F (\underset{˙}{0})$
124		oveq2	$⊢ F (x) = u \to v +_{U} F (x) = v +_{U} u$
125	124	eqeq1d	$⊢ F (x) = u \to (v +_{U} F (x) = F (\underset{˙}{0}) \leftrightarrow v +_{U} u = F (\underset{˙}{0}))$
126	125	rexbidv	$⊢ F (x) = u \to (\exists v \in B v +_{U} F (x) = F (\underset{˙}{0}) \leftrightarrow \exists v \in B v +_{U} u = F (\underset{˙}{0}))$
127	123 126	syl5ibcom	$⊢ (φ \land x \in V) \to (F (x) = u \to \exists v \in B v +_{U} u = F (\underset{˙}{0}))$
128	127	rexlimdva	$⊢ φ \to (\exists x \in V F (x) = u \to \exists v \in B v +_{U} u = F (\underset{˙}{0}))$
129	96 128	sylbid	$⊢ φ \to (u \in B \to \exists v \in B v +_{U} u = F (\underset{˙}{0}))$
130	129	imp	$⊢ (φ \land u \in B) \to \exists v \in B v +_{U} u = F (\underset{˙}{0})$
131	13 14 30 91 94 112 130	isgrpde	$⊢ φ \to U \in Grp$
132	13 14 94 112 131	grpidd2	$⊢ φ \to F (\underset{˙}{0}) = 0_{U}$
133	131 132	jca	$⊢ φ \to (U \in Grp \land F (\underset{˙}{0}) = 0_{U})$

Metamath Proof Explorer

Theorem imasgrp2

Proof