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	⊢ 1 = ( 1_r ‘ 𝑅 )
	rngisom1.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	rngisom1.t	⊢ · = ( ._r ‘ 𝑆 )
Assertion	rngisom1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 1 ) · 𝑥 ) = 𝑥 ∧ ( 𝑥 · ( 𝐹 ‘ 1 ) ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rngisom1.1	⊢ 1 = ( 1_r ‘ 𝑅 )
2		rngisom1.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		rngisom1.t	⊢ · = ( ._r ‘ 𝑆 )
4		rngimcnv	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	2 5	rngimrnghm	⊢ ( ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
7	4 6	syl	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
8	7	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
9	8	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
10	1 2	rngisomfv1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ 1 ) ∈ 𝐵 )
11	10	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ 1 ) ∈ 𝐵 )
12	11	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 1 ) ∈ 𝐵 )
13		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
14		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
15	2 3 14	rnghmmul	⊢ ( ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ ( 𝐹 ‘ 1 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ) = ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) )
16	9 12 13 15	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ) = ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) )
17	16	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) ) )
18	5 2	rngimf1o	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 )
19	18	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 )
20		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ Rng )
21	2 3	rngcl	⊢ ( ( 𝑆 ∈ Rng ∧ ( 𝐹 ‘ 1 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 1 ) · 𝑥 ) ∈ 𝐵 )
22	20 12 13 21	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 1 ) · 𝑥 ) ∈ 𝐵 )
23		f1ocnvfv2	⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ) ) = ( ( 𝐹 ‘ 1 ) · 𝑥 ) )
24	19 22 23	syl2an2r	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( ( 𝐹 ‘ 1 ) · 𝑥 ) ) ) = ( ( 𝐹 ‘ 1 ) · 𝑥 ) )
25	5 1	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
26	25	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 1 ∈ ( Base ‘ 𝑅 ) )
27	19 26	jca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ 1 ∈ ( Base ‘ 𝑅 ) ) )
28	27	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ 1 ∈ ( Base ‘ 𝑅 ) ) )
29		f1ocnvfv1	⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) = 1 )
30	28 29	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) = 1 )
31	30	oveq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) = ( 1 ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) )
32		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
33	2 5	rngimf1o	⊢ ( ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) → ^◡ 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑅 ) )
34		f1of	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑅 ) → ^◡ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
35	33 34	syl	⊢ ( ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) → ^◡ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
36	4 35	syl	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ^◡ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
37	36	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
38	37	ffvelcdmda	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
39	5 14 1 32 38	ringlidmd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 1 ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) = ( ^◡ 𝐹 ‘ 𝑥 ) )
40	31 39	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) = ( ^◡ 𝐹 ‘ 𝑥 ) )
41	40	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) )
42		f1ocnvfv2	⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
43	19 42	sylan	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
44	41 43	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑥 ) ) ) = 𝑥 )
45	17 24 44	3eqtr3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 1 ) · 𝑥 ) = 𝑥 )
46	4	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) )
47	46 6	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
48	47	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
49	2 3 14	rnghmmul	⊢ ( ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 1 ) ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ) )
50	48 13 12 49	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ) )
51	30	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( ._r ‘ 𝑅 ) ( ^◡ 𝐹 ‘ ( 𝐹 ‘ 1 ) ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( ._r ‘ 𝑅 ) 1 ) )
52	5 14 1 32 38	ringridmd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( ._r ‘ 𝑅 ) 1 ) = ( ^◡ 𝐹 ‘ 𝑥 ) )
53	50 51 52	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) = ( ^◡ 𝐹 ‘ 𝑥 ) )
54	53	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) ) = ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) )
55	2 3	rngcl	⊢ ( ( 𝑆 ∈ Rng ∧ 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 1 ) ∈ 𝐵 ) → ( 𝑥 · ( 𝐹 ‘ 1 ) ) ∈ 𝐵 )
56	20 13 12 55	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · ( 𝐹 ‘ 1 ) ) ∈ 𝐵 )
57		f1ocnvfv2	⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ 𝐵 ∧ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) ) = ( 𝑥 · ( 𝐹 ‘ 1 ) ) )
58	19 56 57	syl2an2r	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 · ( 𝐹 ‘ 1 ) ) ) ) = ( 𝑥 · ( 𝐹 ‘ 1 ) ) )
59	54 58 43	3eqtr3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · ( 𝐹 ‘ 1 ) ) = 𝑥 )
60	45 59	jca	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 1 ) · 𝑥 ) = 𝑥 ∧ ( 𝑥 · ( 𝐹 ‘ 1 ) ) = 𝑥 ) )
61	60	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 1 ) · 𝑥 ) = 𝑥 ∧ ( 𝑥 · ( 𝐹 ‘ 1 ) ) = 𝑥 ) )

Metamath Proof Explorer

Theorem rngisom1

Proof