rngisom1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is a ring unity of the non-unital ring. (Contributed by AV, 27-Feb-2025)

	Ref	Expression
Hypotheses	rngisom1.1	$⊢ \underset{˙}{1} = 1_{R}$
	rngisom1.b	$⊢ B = {Base}_{S}$
	rngisom1.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
Assertion	rngisom1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to \forall x \in B (F (\underset{˙}{1}) \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} F (\underset{˙}{1}) = x)$

Proof

Step	Hyp	Ref	Expression
1		rngisom1.1	$⊢ \underset{˙}{1} = 1_{R}$
2		rngisom1.b	$⊢ B = {Base}_{S}$
3		rngisom1.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
4		rngimcnv	$⊢ F \in (R RngIso S) \to F^{-1} \in (S RngIso R)$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	2 5	rngimrnghm	$⊢ F^{-1} \in (S RngIso R) \to F^{-1} \in (S RngHom R)$
7	4 6	syl	$⊢ F \in (R RngIso S) \to F^{-1} \in (S RngHom R)$
8	7	3ad2ant3	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F^{-1} \in (S RngHom R)$
9	8	adantr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} \in (S RngHom R)$
10	1 2	rngisomfv1	$⊢ (R \in Ring \land F \in (R RngIso S)) \to F (\underset{˙}{1}) \in B$
11	10	3adant2	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F (\underset{˙}{1}) \in B$
12	11	adantr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (\underset{˙}{1}) \in B$
13		simpr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to x \in B$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	2 3 14	rnghmmul	$⊢ (F^{-1} \in (S RngHom R) \land F (\underset{˙}{1}) \in B \land x \in B) \to F^{-1} (F (\underset{˙}{1}) \underset{˙}{\cdot} x) = F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x)$
16	9 12 13 15	syl3anc	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (F (\underset{˙}{1}) \underset{˙}{\cdot} x) = F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x)$
17	16	fveq2d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (F (\underset{˙}{1}) \underset{˙}{\cdot} x)) = F (F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x))$
18	5 2	rngimf1o	$⊢ F \in (R RngIso S) \to F : {Base}_{R} \underset{1-1 onto}{⟶} B$
19	18	3ad2ant3	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F : {Base}_{R} \underset{1-1 onto}{⟶} B$
20		simpl2	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to S \in Rng$
21	2 3	rngcl	$⊢ (S \in Rng \land F (\underset{˙}{1}) \in B \land x \in B) \to F (\underset{˙}{1}) \underset{˙}{\cdot} x \in B$
22	20 12 13 21	syl3anc	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (\underset{˙}{1}) \underset{˙}{\cdot} x \in B$
23		f1ocnvfv2	$⊢ (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land F (\underset{˙}{1}) \underset{˙}{\cdot} x \in B) \to F (F^{-1} (F (\underset{˙}{1}) \underset{˙}{\cdot} x)) = F (\underset{˙}{1}) \underset{˙}{\cdot} x$
24	19 22 23	syl2an2r	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (F (\underset{˙}{1}) \underset{˙}{\cdot} x)) = F (\underset{˙}{1}) \underset{˙}{\cdot} x$
25	5 1	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
26	25	3ad2ant1	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to \underset{˙}{1} \in {Base}_{R}$
27	19 26	jca	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land \underset{˙}{1} \in {Base}_{R})$
28	27	adantr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land \underset{˙}{1} \in {Base}_{R})$
29		f1ocnvfv1	$⊢ (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land \underset{˙}{1} \in {Base}_{R}) \to F^{-1} (F (\underset{˙}{1})) = \underset{˙}{1}$
30	28 29	syl	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (F (\underset{˙}{1})) = \underset{˙}{1}$
31	30	oveq1d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x) = \underset{˙}{1} \cdot_{R} F^{-1} (x)$
32		simpl1	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to R \in Ring$
33	2 5	rngimf1o	$⊢ F^{-1} \in (S RngIso R) \to F^{-1} : B \underset{1-1 onto}{⟶} {Base}_{R}$
34		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} {Base}_{R} \to F^{-1} : B ⟶ {Base}_{R}$
35	33 34	syl	$⊢ F^{-1} \in (S RngIso R) \to F^{-1} : B ⟶ {Base}_{R}$
36	4 35	syl	$⊢ F \in (R RngIso S) \to F^{-1} : B ⟶ {Base}_{R}$
37	36	3ad2ant3	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F^{-1} : B ⟶ {Base}_{R}$
38	37	ffvelcdmda	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (x) \in {Base}_{R}$
39	5 14 1 32 38	ringlidmd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to \underset{˙}{1} \cdot_{R} F^{-1} (x) = F^{-1} (x)$
40	31 39	eqtrd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x) = F^{-1} (x)$
41	40	fveq2d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x)) = F (F^{-1} (x))$
42		f1ocnvfv2	$⊢ (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land x \in B) \to F (F^{-1} (x)) = x$
43	19 42	sylan	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (x)) = x$
44	41 43	eqtrd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (F (\underset{˙}{1})) \cdot_{R} F^{-1} (x)) = x$
45	17 24 44	3eqtr3d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (\underset{˙}{1}) \underset{˙}{\cdot} x = x$
46	4	3ad2ant3	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F^{-1} \in (S RngIso R)$
47	46 6	syl	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to F^{-1} \in (S RngHom R)$
48	47	adantr	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} \in (S RngHom R)$
49	2 3 14	rnghmmul	$⊢ (F^{-1} \in (S RngHom R) \land x \in B \land F (\underset{˙}{1}) \in B) \to F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1})) = F^{-1} (x) \cdot_{R} F^{-1} (F (\underset{˙}{1}))$
50	48 13 12 49	syl3anc	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1})) = F^{-1} (x) \cdot_{R} F^{-1} (F (\underset{˙}{1}))$
51	30	oveq2d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (x) \cdot_{R} F^{-1} (F (\underset{˙}{1})) = F^{-1} (x) \cdot_{R} \underset{˙}{1}$
52	5 14 1 32 38	ringridmd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (x) \cdot_{R} \underset{˙}{1} = F^{-1} (x)$
53	50 51 52	3eqtrd	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1})) = F^{-1} (x)$
54	53	fveq2d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1}))) = F (F^{-1} (x))$
55	2 3	rngcl	$⊢ (S \in Rng \land x \in B \land F (\underset{˙}{1}) \in B) \to x \underset{˙}{\cdot} F (\underset{˙}{1}) \in B$
56	20 13 12 55	syl3anc	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to x \underset{˙}{\cdot} F (\underset{˙}{1}) \in B$
57		f1ocnvfv2	$⊢ (F : {Base}_{R} \underset{1-1 onto}{⟶} B \land x \underset{˙}{\cdot} F (\underset{˙}{1}) \in B) \to F (F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1}))) = x \underset{˙}{\cdot} F (\underset{˙}{1})$
58	19 56 57	syl2an2r	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to F (F^{-1} (x \underset{˙}{\cdot} F (\underset{˙}{1}))) = x \underset{˙}{\cdot} F (\underset{˙}{1})$
59	54 58 43	3eqtr3d	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to x \underset{˙}{\cdot} F (\underset{˙}{1}) = x$
60	45 59	jca	$⊢ ((R \in Ring \land S \in Rng \land F \in (R RngIso S)) \land x \in B) \to (F (\underset{˙}{1}) \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} F (\underset{˙}{1}) = x)$
61	60	ralrimiva	$⊢ (R \in Ring \land S \in Rng \land F \in (R RngIso S)) \to \forall x \in B (F (\underset{˙}{1}) \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} F (\underset{˙}{1}) = x)$

Metamath Proof Explorer

Theorem rngisom1

Proof