imasgrp

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))$
	imasgrp.r	$⊢ φ \to R \in Grp$
	imasgrp.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	imasgrp	$⊢ φ \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		imasgrp.r	$⊢ φ \to R \in Grp$
7		imasgrp.z	$⊢ \underset{˙}{0} = 0_{R}$
8	6	3ad2ant1	$⊢ (φ \land x \in V \land y \in V) \to R \in Grp$
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		eqid	$⊢ +_{R} = +_{R}$
16	14 15	grpcl	$⊢ (R \in Grp \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} y \in {Base}_{R}$
17	8 11 13 16	syl3anc	$⊢ (φ \land x \in V \land y \in V) \to x +_{R} y \in {Base}_{R}$
18	3	3ad2ant1	$⊢ (φ \land x \in V \land y \in V) \to \underset{˙}{+} = +_{R}$
19	18	oveqd	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y = x +_{R} y$
20	17 19 10	3eltr4d	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
21	6	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to R \in Grp$
22	11	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \in {Base}_{R}$
23	13	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \in {Base}_{R}$
24		simpr3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in V$
25	2	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to V = {Base}_{R}$
26	24 25	eleqtrd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z \in {Base}_{R}$
27	14 15	grpass	$⊢ (R \in Grp \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x +_{R} y) +_{R} z = x +_{R} (y +_{R} z)$
28	21 22 23 26 27	syl13anc	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (x +_{R} y) +_{R} z = x +_{R} (y +_{R} z)$
29	3	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to \underset{˙}{+} = +_{R}$
30	19	3adant3r3	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} y = x +_{R} y$
31		eqidd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to z = z$
32	29 30 31	oveq123d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = (x +_{R} y) +_{R} z$
33		eqidd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x = x$
34	29	oveqd	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to y \underset{˙}{+} z = y +_{R} z$
35	29 33 34	oveq123d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to x \underset{˙}{+} (y \underset{˙}{+} z) = x +_{R} (y +_{R} z)$
36	28 32 35	3eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
37	36	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))$
38	14 7	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in {Base}_{R}$
39	6 38	syl	$⊢ φ \to \underset{˙}{0} \in {Base}_{R}$
40	39 2	eleqtrrd	$⊢ φ \to \underset{˙}{0} \in V$
41	3	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{+} = +_{R}$
42	41	oveqd	$⊢ (φ \land x \in V) \to \underset{˙}{0} \underset{˙}{+} x = \underset{˙}{0} +_{R} x$
43	2	eleq2d	$⊢ φ \to (x \in V \leftrightarrow x \in {Base}_{R})$
44	43	biimpa	$⊢ (φ \land x \in V) \to x \in {Base}_{R}$
45	14 15 7	grplid	$⊢ (R \in Grp \land x \in {Base}_{R}) \to \underset{˙}{0} +_{R} x = x$
46	6 44 45	syl2an2r	$⊢ (φ \land x \in V) \to \underset{˙}{0} +_{R} x = x$
47	42 46	eqtrd	$⊢ (φ \land x \in V) \to \underset{˙}{0} \underset{˙}{+} x = x$
48	47	fveq2d	$⊢ (φ \land x \in V) \to F (\underset{˙}{0} \underset{˙}{+} x) = F (x)$
49		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
50	14 49	grpinvcl	$⊢ (R \in Grp \land x \in {Base}_{R}) \to {inv}_{g} (R) (x) \in {Base}_{R}$
51	6 44 50	syl2an2r	$⊢ (φ \land x \in V) \to {inv}_{g} (R) (x) \in {Base}_{R}$
52	2	adantr	$⊢ (φ \land x \in V) \to V = {Base}_{R}$
53	51 52	eleqtrrd	$⊢ (φ \land x \in V) \to {inv}_{g} (R) (x) \in V$
54	41	oveqd	$⊢ (φ \land x \in V) \to {inv}_{g} (R) (x) \underset{˙}{+} x = {inv}_{g} (R) (x) +_{R} x$
55	14 15 7 49	grplinv	$⊢ (R \in Grp \land x \in {Base}_{R}) \to {inv}_{g} (R) (x) +_{R} x = \underset{˙}{0}$
56	6 44 55	syl2an2r	$⊢ (φ \land x \in V) \to {inv}_{g} (R) (x) +_{R} x = \underset{˙}{0}$
57	54 56	eqtrd	$⊢ (φ \land x \in V) \to {inv}_{g} (R) (x) \underset{˙}{+} x = \underset{˙}{0}$
58	57	fveq2d	$⊢ (φ \land x \in V) \to F ({inv}_{g} (R) (x) \underset{˙}{+} x) = F (\underset{˙}{0})$
59	1 2 3 4 5 6 20 37 40 48 53 58	imasgrp2	$⊢ φ \to (U \in Grp \land F (\underset{˙}{0}) = 0_{U})$

Metamath Proof Explorer

Theorem imasgrp

Proof