rngisomring1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the ring unity of the second ring is the function value of the ring unity of the first ring for the isomorphism. (Contributed by AV, 16-Mar-2025)

		Ref	Expression
	Assertion	rngisomring1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to 1_{S} = F (1_{R})$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1_{R} = 1_{R}$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3		eqid	$⊢ \cdot_{S} = \cdot_{S}$
4	1 2 3	rngisom1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)$
5		eqidd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to {Base}_{S} = {Base}_{S}$
6		eqidd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to \cdot_{S} = \cdot_{S}$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7 2	rngimf1o	$⊢ F \in (R RngIso S) \to F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}$
9		f1of	$⊢ F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to F : {Base}_{R} ⟶ {Base}_{S}$
10	8 9	syl	$⊢ F \in (R RngIso S) \to F : {Base}_{R} ⟶ {Base}_{S}$
11	10	3ad2ant3	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F : {Base}_{R} ⟶ {Base}_{S}$
12	7 1	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
13	12	3ad2ant1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to 1_{R} \in {Base}_{R}$
14	11 13	ffvelcdmd	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F (1_{R}) \in {Base}_{S}$
15	14	adantr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to F (1_{R}) \in {Base}_{S}$
16		oveq2	$⊢ x = y \to F (1_{R}) \cdot_{S} x = F (1_{R}) \cdot_{S} y$
17		id	$⊢ x = y \to x = y$
18	16 17	eqeq12d	$⊢ x = y \to (F (1_{R}) \cdot_{S} x = x \leftrightarrow F (1_{R}) \cdot_{S} y = y)$
19		oveq1	$⊢ x = y \to x \cdot_{S} F (1_{R}) = y \cdot_{S} F (1_{R})$
20	19 17	eqeq12d	$⊢ x = y \to (x \cdot_{S} F (1_{R}) = x \leftrightarrow y \cdot_{S} F (1_{R}) = y)$
21	18 20	anbi12d	$⊢ x = y \to ((F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x) \leftrightarrow (F (1_{R}) \cdot_{S} y = y \land y \cdot_{S} F (1_{R}) = y))$
22	21	rspccv	$⊢ \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x) \to (y \in {Base}_{S} \to (F (1_{R}) \cdot_{S} y = y \land y \cdot_{S} F (1_{R}) = y))$
23	22	adantl	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to (y \in {Base}_{S} \to (F (1_{R}) \cdot_{S} y = y \land y \cdot_{S} F (1_{R}) = y))$
24		simpl	$⊢ (F (1_{R}) \cdot_{S} y = y \land y \cdot_{S} F (1_{R}) = y) \to F (1_{R}) \cdot_{S} y = y$
25	23 24	syl6	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to (y \in {Base}_{S} \to F (1_{R}) \cdot_{S} y = y)$
26	25	imp	$⊢ (((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \land y \in {Base}_{S}) \to F (1_{R}) \cdot_{S} y = y$
27		simpr	$⊢ (F (1_{R}) \cdot_{S} y = y \land y \cdot_{S} F (1_{R}) = y) \to y \cdot_{S} F (1_{R}) = y$
28	23 27	syl6	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to (y \in {Base}_{S} \to y \cdot_{S} F (1_{R}) = y)$
29	28	imp	$⊢ (((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \land y \in {Base}_{S}) \to y \cdot_{S} F (1_{R}) = y$
30	5 6 15 26 29	ringurd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land \forall x \in {Base}_{S} (F (1_{R}) \cdot_{S} x = x \land x \cdot_{S} F (1_{R}) = x)) \to F (1_{R}) = 1_{S}$
31	4 30	mpdan	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F (1_{R}) = 1_{S}$
32	31	eqcomd	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to 1_{S} = F (1_{R})$

Metamath Proof Explorer

Theorem rngisomring1

Proof