imasaddf

Description: The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	imasaddf.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasaddf.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{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
	imasaddf.u	$⊢ φ \to U = F “_{𝑠} R$
	imasaddf.v	$⊢ φ \to V = {Base}_{R}$
	imasaddf.r	$⊢ φ \to R \in Z$
	imasaddf.p	$⊢ \underset{˙}{\cdot} = +_{R}$
	imasaddf.a	$⊢ \underset{˙}{∙} = +_{U}$
	imasaddf.c	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{\cdot} q \in V$
Assertion	imasaddf	$⊢ φ \to \underset{˙}{∙} : B \times B ⟶ B$

Step	Hyp	Ref	Expression
1		imasaddf.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
2		imasaddf.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{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
3		imasaddf.u	$⊢ φ \to U = F “_{𝑠} R$
4		imasaddf.v	$⊢ φ \to V = {Base}_{R}$
5		imasaddf.r	$⊢ φ \to R \in Z$
6		imasaddf.p	$⊢ \underset{˙}{\cdot} = +_{R}$
7		imasaddf.a	$⊢ \underset{˙}{∙} = +_{U}$
8		imasaddf.c	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{\cdot} q \in V$
9	3 4 1 5 6 7	imasplusg	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
10	1 2 9 8	imasaddflem	$⊢ φ \to \underset{˙}{∙} : B \times B ⟶ B$

Metamath Proof Explorer