exidresid

Description: The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	exidres.1	$⊢ X = ran G$
	exidres.2	$⊢ U = GId (G)$
	exidres.3	$⊢ H = {G ↾}_{(Y \times Y)}$
Assertion	exidresid	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to GId (H) = U$

Proof

Step	Hyp	Ref	Expression
1		exidres.1	$⊢ X = ran G$
2		exidres.2	$⊢ U = GId (G)$
3		exidres.3	$⊢ H = {G ↾}_{(Y \times Y)}$
4		resexg	$⊢ G \in (Magma \cap ExId) \to {G ↾}_{(Y \times Y)} \in V$
5	3 4	eqeltrid	$⊢ G \in (Magma \cap ExId) \to H \in V$
6		eqid	$⊢ ran H = ran H$
7	6	gidval	$⊢ H \in V \to GId (H) = (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x))$
8	5 7	syl	$⊢ G \in (Magma \cap ExId) \to GId (H) = (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x))$
9	8	3ad2ant1	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to GId (H) = (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x))$
10	9	adantr	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to GId (H) = (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x))$
11	1 2 3	exidreslem	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (U \in dom dom H \land \forall x \in dom dom H (U H x = x \land x H U = x))$
12	11	simprd	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to \forall x \in dom dom H (U H x = x \land x H U = x)$
13	12	adantr	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to \forall x \in dom dom H (U H x = x \land x H U = x)$
14	1 2 3	exidres	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to H \in ExId$
15		elin	$⊢ H \in (Magma \cap ExId) \leftrightarrow (H \in Magma \land H \in ExId)$
16		rngopidOLD	$⊢ H \in (Magma \cap ExId) \to ran H = dom dom H$
17	15 16	sylbir	$⊢ (H \in Magma \land H \in ExId) \to ran H = dom dom H$
18	17	ancoms	$⊢ (H \in ExId \land H \in Magma) \to ran H = dom dom H$
19	14 18	sylan	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to ran H = dom dom H$
20	19	raleqdv	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to (\forall x \in ran H (U H x = x \land x H U = x) \leftrightarrow \forall x \in dom dom H (U H x = x \land x H U = x))$
21	13 20	mpbird	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to \forall x \in ran H (U H x = x \land x H U = x)$
22	11	simpld	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to U \in dom dom H$
23	22	adantr	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to U \in dom dom H$
24	23 19	eleqtrrd	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to U \in ran H$
25	6	exidu1	$⊢ H \in (Magma \cap ExId) \to \exists! u \in ran H \forall x \in ran H (u H x = x \land x H u = x)$
26	15 25	sylbir	$⊢ (H \in Magma \land H \in ExId) \to \exists! u \in ran H \forall x \in ran H (u H x = x \land x H u = x)$
27	26	ancoms	$⊢ (H \in ExId \land H \in Magma) \to \exists! u \in ran H \forall x \in ran H (u H x = x \land x H u = x)$
28	14 27	sylan	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to \exists! u \in ran H \forall x \in ran H (u H x = x \land x H u = x)$
29		oveq1	$⊢ u = U \to u H x = U H x$
30	29	eqeq1d	$⊢ u = U \to (u H x = x \leftrightarrow U H x = x)$
31	30	ovanraleqv	$⊢ u = U \to (\forall x \in ran H (u H x = x \land x H u = x) \leftrightarrow \forall x \in ran H (U H x = x \land x H U = x))$
32	31	riota2	$⊢ (U \in ran H \land \exists! u \in ran H \forall x \in ran H (u H x = x \land x H u = x)) \to (\forall x \in ran H (U H x = x \land x H U = x) \leftrightarrow (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x)) = U)$
33	24 28 32	syl2anc	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to (\forall x \in ran H (U H x = x \land x H U = x) \leftrightarrow (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x)) = U)$
34	21 33	mpbid	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to (ι u \in ran H \| \forall x \in ran H (u H x = x \land x H u = x)) = U$
35	10 34	eqtrd	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \land H \in Magma) \to GId (H) = U$

Metamath Proof Explorer

Theorem exidresid

Proof