Theorem pzriprngALT

Description: The non-unital ring ( ZZring Xs. ZZring ) is unital because it has the two-sided ideal ( ZZ X. { 0 } ) , which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb ). (Contributed by AV, 23-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	pzriprngALT	⊢ ( ℤring ×s ℤring ) ∈ Ring

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ℤring ×s ℤring ) ↾s 𝑖 ) = ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) )
2	1	eleq1d	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ↔ ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ∈ Ring ) )
3		oveq2	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ℤring ×s ℤring ) ~QG 𝑖 ) = ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) )
4	3	oveq2d	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) = ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) )
5	4	eleq1d	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring ↔ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) ∈ Ring ) )
6	2 5	anbi12d	⊢ ( 𝑖 = ( ℤ × { 0 } ) → ( ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring ) ↔ ( ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) ∈ Ring ) ) )
7		eqid	⊢ ( ℤring ×s ℤring ) = ( ℤring ×s ℤring )
8		eqid	⊢ ( ℤ × { 0 } ) = ( ℤ × { 0 } )
9		eqid	⊢ ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) = ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) )
10	7 8 9	pzriprnglem8	⊢ ( ℤ × { 0 } ) ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) )
11	10	a1i	⊢ ( ⊤ → ( ℤ × { 0 } ) ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) ) )
12	7 8 9	pzriprnglem7	⊢ ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ∈ Ring
13	12	a1i	⊢ ( ⊤ → ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ∈ Ring )
14		eqid	⊢ ( 1r ‘ ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ) = ( 1r ‘ ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) )
15		eqid	⊢ ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) = ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) )
16		eqid	⊢ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) = ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) )
17	7 8 9 14 15 16	pzriprnglem13	⊢ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) ∈ Ring
18	13 17	jctir	⊢ ( ⊤ → ( ( ( ℤring ×s ℤring ) ↾s ( ℤ × { 0 } ) ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG ( ℤ × { 0 } ) ) ) ∈ Ring ) )
19	6 11 18	rspcedvdw	⊢ ( ⊤ → ∃ 𝑖 ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) ) ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring ) )
20	19	mptru	⊢ ∃ 𝑖 ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) ) ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring )
21	7	pzriprnglem1	⊢ ( ℤring ×s ℤring ) ∈ Rng
22		ring2idlqusb	⊢ ( ( ℤring ×s ℤring ) ∈ Rng → ( ( ℤring ×s ℤring ) ∈ Ring ↔ ∃ 𝑖 ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) ) ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring ) ) )
23	21 22	ax-mp	⊢ ( ( ℤring ×s ℤring ) ∈ Ring ↔ ∃ 𝑖 ∈ ( 2Ideal ‘ ( ℤring ×s ℤring ) ) ( ( ( ℤring ×s ℤring ) ↾s 𝑖 ) ∈ Ring ∧ ( ( ℤring ×s ℤring ) /s ( ( ℤring ×s ℤring ) ~QG 𝑖 ) ) ∈ Ring ) )
24	20 23	mpbir	⊢ ( ℤring ×s ℤring ) ∈ Ring