Metamath Proof Explorer

Theorem grpinv11OLD

Description: Obsolete version of grpinv11 as of 8-Jul-2025. (Contributed by NM, 22-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	grpinvinv.b	$⊢ B = {Base}_{G}$
		grpinvinv.n	$⊢ N = {inv}_{g} (G)$
		grpinv11.g	$⊢ φ \to G \in Grp$
		grpinv11.x	$⊢ φ \to X \in B$
		grpinv11.y	$⊢ φ \to Y \in B$
	Assertion	grpinv11OLD	$⊢ φ \to (N (X) = N (Y) \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	$⊢ B = {Base}_{G}$
2		grpinvinv.n	$⊢ N = {inv}_{g} (G)$
3		grpinv11.g	$⊢ φ \to G \in Grp$
4		grpinv11.x	$⊢ φ \to X \in B$
5		grpinv11.y	$⊢ φ \to Y \in B$
6		fveq2	$⊢ N (X) = N (Y) \to N (N (X)) = N (N (Y))$
7	6	adantl	$⊢ (φ \land N (X) = N (Y)) \to N (N (X)) = N (N (Y))$
8	1 2	grpinvinv	$⊢ (G \in Grp \land X \in B) \to N (N (X)) = X$
9	3 4 8	syl2anc	$⊢ φ \to N (N (X)) = X$
10	9	adantr	$⊢ (φ \land N (X) = N (Y)) \to N (N (X)) = X$
11	1 2	grpinvinv	$⊢ (G \in Grp \land Y \in B) \to N (N (Y)) = Y$
12	3 5 11	syl2anc	$⊢ φ \to N (N (Y)) = Y$
13	12	adantr	$⊢ (φ \land N (X) = N (Y)) \to N (N (Y)) = Y$
14	7 10 13	3eqtr3d	$⊢ (φ \land N (X) = N (Y)) \to X = Y$
15	14	ex	$⊢ φ \to (N (X) = N (Y) \to X = Y)$
16		fveq2	$⊢ X = Y \to N (X) = N (Y)$
17	15 16	impbid1	$⊢ φ \to (N (X) = N (Y) \leftrightarrow X = Y)$