Metamath Proof Explorer

Theorem rngisomring

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then both rings are unital. (Contributed by AV, 27-Feb-2025)

		Ref	Expression
	Assertion	rngisomring	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to S \in Ring$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to S \in Rng$
2		eqid	$⊢ 1_{R} = 1_{R}$
3		eqid	$⊢ {Base}_{S} = {Base}_{S}$
4	2 3	rngisomfv1	$⊢ (R \in Ring \land F \in (R RngIsom S)) \to F (1_{R}) \in {Base}_{S}$
5	4	3adant2	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to F (1_{R}) \in {Base}_{S}$
6		oveq1	$⊢ i = F (1_{R}) \to i \cdot_{S} x = F (1_{R}) \cdot_{S} x$
7	6	eqeq1d	$⊢ i = F (1_{R}) \to (i \cdot_{S} x = x \leftrightarrow F (1_{R}) \cdot_{S} x = x)$
8		oveq2	$⊢ i = F (1_{R}) \to x \cdot_{S} i = x \cdot_{S} F (1_{R})$
9	8	eqeq1d	$⊢ i = F (1_{R}) \to (x \cdot_{S} i = x \leftrightarrow x \cdot_{S} F (1_{R}) = x)$
10	7 9	anbi12d	$⊢ i = F (1_{R}) \to ((i \cdot_{S} x = x \land x \cdot_{S} i = x) \leftrightarrow (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x))$
11	10	ralbidv	$⊢ i = F (1_{R}) \to (\forall x \in {Base}_{S} (i \cdot_{S} x = x \land x \cdot_{S} i = x) \leftrightarrow \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x))$
12	11	adantl	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \land i = F (1_{R})) \to (\forall x \in {Base}_{S} (i \cdot_{S} x = x \land x \cdot_{S} i = x) \leftrightarrow \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x))$
13		eqid	$⊢ \cdot_{S} = \cdot_{S}$
14	2 3 13	rngisom1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)$
15	5 12 14	rspcedvd	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to \exists i \in {Base}_{S} \forall x \in {Base}_{S} (i \cdot_{S} x = x \land x \cdot_{S} i = x)$
16	3 13	isringrng	$⊢ S \in Ring \leftrightarrow (S \in Rng \land \exists i \in {Base}_{S} \forall x \in {Base}_{S} (i \cdot_{S} x = x \land x \cdot_{S} i = x))$
17	1 15 16	sylanbrc	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIsom S)) \to S \in Ring$