imasabl

Description: The image structure of an abelian group is an abelian group ( imasgrp analog). (Contributed by AV, 22-Feb-2025)

	Ref	Expression
Hypotheses	imasabl.u	$⊢ φ \to U = F “_{𝑠} R$
	imasabl.v	$⊢ φ \to V = {Base}_{R}$
	imasabl.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	imasabl.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasabl.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))$
	imasabl.r	$⊢ φ \to R \in Abel$
	imasabl.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	imasabl	$⊢ φ \to (U \in Abel \land F (\underset{˙}{0}) = 0_{U})$

Proof

Step	Hyp	Ref	Expression
1		imasabl.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasabl.v	$⊢ φ \to V = {Base}_{R}$
3		imasabl.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
4		imasabl.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
5		imasabl.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		imasabl.r	$⊢ φ \to R \in Abel$
7		imasabl.z	$⊢ \underset{˙}{0} = 0_{R}$
8	6	ablgrpd	$⊢ φ \to R \in Grp$
9	1 2 3 4 5 8 7	imasgrp	$⊢ φ \to (U \in Grp \land F (\underset{˙}{0}) = 0_{U})$
10	1 2 4 6	imasbas	$⊢ φ \to B = {Base}_{U}$
11	10	eqcomd	$⊢ φ \to {Base}_{U} = B$
12	11	eleq2d	$⊢ φ \to (x \in {Base}_{U} \leftrightarrow x \in B)$
13	11	eleq2d	$⊢ φ \to (y \in {Base}_{U} \leftrightarrow y \in B)$
14	12 13	anbi12d	$⊢ φ \to ((x \in {Base}_{U} \land y \in {Base}_{U}) \leftrightarrow (x \in B \land y \in B))$
15	14	adantr	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to ((x \in {Base}_{U} \land y \in {Base}_{U}) \leftrightarrow (x \in B \land y \in B))$
16		foelcdmi	$⊢ (F : V \underset{onto}{⟶} B \land x \in B) \to \exists a \in V F (a) = x$
17	16	ex	$⊢ F : V \underset{onto}{⟶} B \to (x \in B \to \exists a \in V F (a) = x)$
18		foelcdmi	$⊢ (F : V \underset{onto}{⟶} B \land y \in B) \to \exists b \in V F (b) = y$
19	18	ex	$⊢ F : V \underset{onto}{⟶} B \to (y \in B \to \exists b \in V F (b) = y)$
20	17 19	anim12d	$⊢ F : V \underset{onto}{⟶} B \to ((x \in B \land y \in B) \to (\exists a \in V F (a) = x \land \exists b \in V F (b) = y))$
21	4 20	syl	$⊢ φ \to ((x \in B \land y \in B) \to (\exists a \in V F (a) = x \land \exists b \in V F (b) = y))$
22	21	adantr	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to ((x \in B \land y \in B) \to (\exists a \in V F (a) = x \land \exists b \in V F (b) = y))$
23	6	ad3antrrr	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to R \in Abel$
24	2	eleq2d	$⊢ φ \to (a \in V \leftrightarrow a \in {Base}_{R})$
25	24	biimpd	$⊢ φ \to (a \in V \to a \in {Base}_{R})$
26	25	adantr	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to (a \in V \to a \in {Base}_{R})$
27	26	imp	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \to a \in {Base}_{R}$
28	27	adantr	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to a \in {Base}_{R}$
29	2	eleq2d	$⊢ φ \to (b \in V \leftrightarrow b \in {Base}_{R})$
30	29	biimpd	$⊢ φ \to (b \in V \to b \in {Base}_{R})$
31	30	adantr	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to (b \in V \to b \in {Base}_{R})$
32	31	adantr	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \to (b \in V \to b \in {Base}_{R})$
33	32	imp	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to b \in {Base}_{R}$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35		eqid	$⊢ +_{R} = +_{R}$
36	34 35	ablcom	$⊢ (R \in Abel \land a \in {Base}_{R} \land b \in {Base}_{R}) \to a +_{R} b = b +_{R} a$
37	23 28 33 36	syl3anc	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to a +_{R} b = b +_{R} a$
38	37	fveq2d	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to F (a +_{R} b) = F (b +_{R} a)$
39		simplll	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to φ$
40		simpr	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \to a \in V$
41	40	adantr	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to a \in V$
42		simpr	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to b \in V$
43	3	eqcomd	$⊢ φ \to +_{R} = \underset{˙}{+}$
44	43	oveqd	$⊢ φ \to a +_{R} b = a \underset{˙}{+} b$
45	44	fveq2d	$⊢ φ \to F (a +_{R} b) = F (a \underset{˙}{+} b)$
46	43	oveqd	$⊢ φ \to p +_{R} q = p \underset{˙}{+} q$
47	46	fveq2d	$⊢ φ \to F (p +_{R} q) = F (p \underset{˙}{+} q)$
48	45 47	eqeq12d	$⊢ φ \to (F (a +_{R} b) = F (p +_{R} q) \leftrightarrow F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
49	48	3ad2ant1	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (F (a +_{R} b) = F (p +_{R} q) \leftrightarrow F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
50	5 49	sylibrd	$⊢ (φ \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))$
51		eqid	$⊢ +_{U} = +_{U}$
52	4 50 1 2 6 35 51	imasaddval	$⊢ (φ \land a \in V \land b \in V) \to F (a) +_{U} F (b) = F (a +_{R} b)$
53	39 41 42 52	syl3anc	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to F (a) +_{U} F (b) = F (a +_{R} b)$
54	4 50 1 2 6 35 51	imasaddval	$⊢ (φ \land b \in V \land a \in V) \to F (b) +_{U} F (a) = F (b +_{R} a)$
55	39 42 41 54	syl3anc	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to F (b) +_{U} F (a) = F (b +_{R} a)$
56	38 53 55	3eqtr4d	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to F (a) +_{U} F (b) = F (b) +_{U} F (a)$
57	56	adantr	$⊢ ((((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \land (F (b) = y \land F (a) = x)) \to F (a) +_{U} F (b) = F (b) +_{U} F (a)$
58		oveq12	$⊢ (F (a) = x \land F (b) = y) \to F (a) +_{U} F (b) = x +_{U} y$
59	58	ancoms	$⊢ (F (b) = y \land F (a) = x) \to F (a) +_{U} F (b) = x +_{U} y$
60		oveq12	$⊢ (F (b) = y \land F (a) = x) \to F (b) +_{U} F (a) = y +_{U} x$
61	59 60	eqeq12d	$⊢ (F (b) = y \land F (a) = x) \to (F (a) +_{U} F (b) = F (b) +_{U} F (a) \leftrightarrow x +_{U} y = y +_{U} x)$
62	61	adantl	$⊢ ((((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \land (F (b) = y \land F (a) = x)) \to (F (a) +_{U} F (b) = F (b) +_{U} F (a) \leftrightarrow x +_{U} y = y +_{U} x)$
63	57 62	mpbid	$⊢ ((((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \land (F (b) = y \land F (a) = x)) \to x +_{U} y = y +_{U} x$
64	63	exp32	$⊢ (((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \land b \in V) \to (F (b) = y \to (F (a) = x \to x +_{U} y = y +_{U} x))$
65	64	rexlimdva	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \to (\exists b \in V F (b) = y \to (F (a) = x \to x +_{U} y = y +_{U} x))$
66	65	com23	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land a \in V) \to (F (a) = x \to (\exists b \in V F (b) = y \to x +_{U} y = y +_{U} x))$
67	66	rexlimdva	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to (\exists a \in V F (a) = x \to (\exists b \in V F (b) = y \to x +_{U} y = y +_{U} x))$
68	67	impd	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to ((\exists a \in V F (a) = x \land \exists b \in V F (b) = y) \to x +_{U} y = y +_{U} x)$
69	22 68	syld	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to ((x \in B \land y \in B) \to x +_{U} y = y +_{U} x)$
70	15 69	sylbid	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to ((x \in {Base}_{U} \land y \in {Base}_{U}) \to x +_{U} y = y +_{U} x)$
71	70	imp	$⊢ ((φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \land (x \in {Base}_{U} \land y \in {Base}_{U})) \to x +_{U} y = y +_{U} x$
72	71	ralrimivva	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to \forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x$
73		simpr	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to (U \in Grp \land F (\underset{˙}{0}) = 0_{U})$
74	72 73	jca	$⊢ (φ \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U})) \to (\forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U}))$
75	9 74	mpdan	$⊢ φ \to (\forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U}))$
76		eqid	$⊢ {Base}_{U} = {Base}_{U}$
77	76 51	isabl2	$⊢ U \in Abel \leftrightarrow (U \in Grp \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x)$
78	77	anbi1i	$⊢ (U \in Abel \land F (\underset{˙}{0}) = 0_{U}) \leftrightarrow ((U \in Grp \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x) \land F (\underset{˙}{0}) = 0_{U})$
79		an21	$⊢ ((U \in Grp \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x) \land F (\underset{˙}{0}) = 0_{U}) \leftrightarrow (\forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U}))$
80	78 79	bitri	$⊢ (U \in Abel \land F (\underset{˙}{0}) = 0_{U}) \leftrightarrow (\forall x \in {Base}_{U} \forall y \in {Base}_{U} x +_{U} y = y +_{U} x \land (U \in Grp \land F (\underset{˙}{0}) = 0_{U}))$
81	75 80	sylibr	$⊢ φ \to (U \in Abel \land F (\underset{˙}{0}) = 0_{U})$

Metamath Proof Explorer

Theorem imasabl

Proof