Theorem pzriprnglem13

Description: Lemma 13 for pzriprng : Q is a unital ring. (Contributed by AV, 23-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
	pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
	pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	pzriprng.1	⊢ 1 = ( 1r ‘ 𝐽 )
	pzriprng.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	pzriprng.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
Assertion	pzriprnglem13	⊢ 𝑄 ∈ Ring

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
3		pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		pzriprng.1	⊢ 1 = ( 1r ‘ 𝐽 )
5		pzriprng.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
6		pzriprng.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
7	1	pzriprnglem1	⊢ 𝑅 ∈ Rng
8	1 2 3	pzriprnglem8	⊢ 𝐼 ∈ ( 2Ideal ‘ 𝑅 )
9	1 2	pzriprnglem4	⊢ 𝐼 ∈ ( SubGrp ‘ 𝑅 )
10	5	oveq2i	⊢ ( 𝑅 /s ∼ ) = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
11	6 10	eqtri	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
12		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
13	11 12	qus2idrng	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑄 ∈ Rng )
14	7 8 9 13	mp3an	⊢ 𝑄 ∈ Rng
15		1z	⊢ 1 ∈ ℤ
16		zex	⊢ ℤ ∈ V
17		snex	⊢ { 1 } ∈ V
18	16 17	xpex	⊢ ( ℤ × { 1 } ) ∈ V
19	18	snid	⊢ ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) }
20		sneq	⊢ ( 𝑦 = 1 → { 𝑦 } = { 1 } )
21	20	xpeq2d	⊢ ( 𝑦 = 1 → ( ℤ × { 𝑦 } ) = ( ℤ × { 1 } ) )
22	21	sneqd	⊢ ( 𝑦 = 1 → { ( ℤ × { 𝑦 } ) } = { ( ℤ × { 1 } ) } )
23	22	eleq2d	⊢ ( 𝑦 = 1 → ( ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } ↔ ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) } ) )
24	23	rspcev	⊢ ( ( 1 ∈ ℤ ∧ ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) } ) → ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } )
25	15 19 24	mp2an	⊢ ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) }
26		eliun	⊢ ( ( ℤ × { 1 } ) ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) } ↔ ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } )
27	25 26	mpbir	⊢ ( ℤ × { 1 } ) ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) }
28	1 2 3 4 5 6	pzriprnglem11	⊢ ( Base ‘ 𝑄 ) = ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) }
29	27 28	eleqtrri	⊢ ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 )
30		oveq1	⊢ ( 𝑖 = ( ℤ × { 1 } ) → ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) )
31	30	eqeq1d	⊢ ( 𝑖 = ( ℤ × { 1 } ) → ( ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ↔ ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ) )
32	31	ovanraleqv	⊢ ( 𝑖 = ( ℤ × { 1 } ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) 𝑖 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) ) )
33		id	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) → ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) )
34	1 2 3 4 5 6	pzriprnglem12	⊢ ( 𝑥 ∈ ( Base ‘ 𝑄 ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) )
35	34	a1i	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) → ( 𝑥 ∈ ( Base ‘ 𝑄 ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) ) )
36	35	ralrimiv	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) )
37	32 33 36	rspcedvdw	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑄 ) ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) 𝑖 ) = 𝑥 ) )
38	29 37	ax-mp	⊢ ∃ 𝑖 ∈ ( Base ‘ 𝑄 ) ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) 𝑖 ) = 𝑥 )
39		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
40		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
41	39 40	isringrng	⊢ ( 𝑄 ∈ Ring ↔ ( 𝑄 ∈ Rng ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑄 ) ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( 𝑖 ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) 𝑖 ) = 𝑥 ) ) )
42	14 38 41	mpbir2an	⊢ 𝑄 ∈ Ring