Theorem pzriprnglem14

Description: Lemma 14 for pzriprng : The ring unity of the ring Q . (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	pzriprnglem14	⊢ ( 1r ‘ 𝑄 ) = ( ℤ × { 1 } )

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		1z	⊢ 1 ∈ ℤ
8		sneq	⊢ ( 𝑦 = 1 → { 𝑦 } = { 1 } )
9	8	xpeq2d	⊢ ( 𝑦 = 1 → ( ℤ × { 𝑦 } ) = ( ℤ × { 1 } ) )
10	9	sneqd	⊢ ( 𝑦 = 1 → { ( ℤ × { 𝑦 } ) } = { ( ℤ × { 1 } ) } )
11	10	eleq2d	⊢ ( 𝑦 = 1 → ( ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } ↔ ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) } ) )
12		id	⊢ ( 1 ∈ ℤ → 1 ∈ ℤ )
13		zex	⊢ ℤ ∈ V
14		snex	⊢ { 1 } ∈ V
15	13 14	xpex	⊢ ( ℤ × { 1 } ) ∈ V
16	15	snid	⊢ ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) }
17	16	a1i	⊢ ( 1 ∈ ℤ → ( ℤ × { 1 } ) ∈ { ( ℤ × { 1 } ) } )
18	11 12 17	rspcedvdw	⊢ ( 1 ∈ ℤ → ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } )
19	7 18	ax-mp	⊢ ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) }
20	1 2 3 4 5 6	pzriprnglem11	⊢ ( Base ‘ 𝑄 ) = ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) }
21	20	eleq2i	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) ↔ ( ℤ × { 1 } ) ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) } )
22		eliun	⊢ ( ( ℤ × { 1 } ) ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) } ↔ ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } )
23	21 22	bitri	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) ↔ ∃ 𝑦 ∈ ℤ ( ℤ × { 1 } ) ∈ { ( ℤ × { 𝑦 } ) } )
24	19 23	mpbir	⊢ ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 )
25	1 2 3 4 5 6	pzriprnglem12	⊢ ( 𝑥 ∈ ( Base ‘ 𝑄 ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) )
26	25	rgen	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 )
27	24 26	pm3.2i	⊢ ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) )
28	1 2 3 4 5 6	pzriprnglem13	⊢ 𝑄 ∈ Ring
29		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
30		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
31		eqid	⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
32	29 30 31	isringid	⊢ ( 𝑄 ∈ Ring → ( ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝑄 ) = ( ℤ × { 1 } ) ) )
33	28 32	ax-mp	⊢ ( ( ( ℤ × { 1 } ) ∈ ( Base ‘ 𝑄 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑄 ) ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝑄 ) = ( ℤ × { 1 } ) )
34	27 33	mpbi	⊢ ( 1r ‘ 𝑄 ) = ( ℤ × { 1 } )