Theorem pzriprnglem11

Description: Lemma 11 for pzriprng : The base set of the quotient of R and J . (Contributed by AV, 22-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	pzriprnglem11	⊢ ( Base ‘ 𝑄 ) = ∪ 𝑟 ∈ ℤ { ( ℤ × { 𝑟 } ) }

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		df-qs	⊢ ( ( ℤ × ℤ ) / ∼ ) = { 𝑒 ∣ ∃ 𝑝 ∈ ( ℤ × ℤ ) 𝑒 = [ 𝑝 ] ∼ }
8	6	a1i	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → 𝑄 = ( 𝑅 /s ∼ ) )
9	1	pzriprnglem2	⊢ ( Base ‘ 𝑅 ) = ( ℤ × ℤ )
10	9	eqcomi	⊢ ( ℤ × ℤ ) = ( Base ‘ 𝑅 )
11	10	a1i	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → ( ℤ × ℤ ) = ( Base ‘ 𝑅 ) )
12		ovexd	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → ( 𝑅 ~QG 𝐼 ) ∈ V )
13	5 12	eqeltrid	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → ∼ ∈ V )
14	1	pzriprnglem1	⊢ 𝑅 ∈ Rng
15	14	a1i	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → 𝑅 ∈ Rng )
16	8 11 13 15	qusbas	⊢ ( ∼ = ( 𝑅 ~QG 𝐼 ) → ( ( ℤ × ℤ ) / ∼ ) = ( Base ‘ 𝑄 ) )
17	5 16	ax-mp	⊢ ( ( ℤ × ℤ ) / ∼ ) = ( Base ‘ 𝑄 )
18		nfcv	⊢ Ⅎ 𝑠 { 𝑒 ∣ 𝑒 = [ 𝑝 ] ∼ }
19		nfcv	⊢ Ⅎ 𝑟 { 𝑒 ∣ 𝑒 = [ 𝑝 ] ∼ }
20		nfcv	⊢ Ⅎ 𝑝 { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
21		eceq1	⊢ ( 𝑝 = ⟨ 𝑠 , 𝑟 ⟩ → [ 𝑝 ] ∼ = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ )
22	21	eqeq2d	⊢ ( 𝑝 = ⟨ 𝑠 , 𝑟 ⟩ → ( 𝑒 = [ 𝑝 ] ∼ ↔ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ) )
23	22	abbidv	⊢ ( 𝑝 = ⟨ 𝑠 , 𝑟 ⟩ → { 𝑒 ∣ 𝑒 = [ 𝑝 ] ∼ } = { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } )
24	18 19 20 23	iunxpf	⊢ ∪ 𝑝 ∈ ( ℤ × ℤ ) { 𝑒 ∣ 𝑒 = [ 𝑝 ] ∼ } = ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
25		iunab	⊢ ∪ 𝑝 ∈ ( ℤ × ℤ ) { 𝑒 ∣ 𝑒 = [ 𝑝 ] ∼ } = { 𝑒 ∣ ∃ 𝑝 ∈ ( ℤ × ℤ ) 𝑒 = [ 𝑝 ] ∼ }
26		iuncom	⊢ ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = ∪ 𝑟 ∈ ℤ ∪ 𝑠 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
27		df-sn	⊢ { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
28	27	eqcomi	⊢ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
29	28	a1i	⊢ ( 𝑠 ∈ ℤ → { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } )
30	29	iuneq2i	⊢ ∪ 𝑠 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = ∪ 𝑠 ∈ ℤ { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
31		simpr	⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ∧ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ) → 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ )
32	1 2 3 4 5	pzriprnglem10	⊢ ( ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ = ( ℤ × { 𝑟 } ) )
33	32	ancoms	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ = ( ℤ × { 𝑟 } ) )
34	33	adantr	⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ∧ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ) → [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ = ( ℤ × { 𝑟 } ) )
35	31 34	eqtrd	⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ∧ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ) → 𝑝 = ( ℤ × { 𝑟 } ) )
36	35	ex	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ → 𝑝 = ( ℤ × { 𝑟 } ) ) )
37	36	rexlimdva	⊢ ( 𝑟 ∈ ℤ → ( ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ → 𝑝 = ( ℤ × { 𝑟 } ) ) )
38		0zd	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 = ( ℤ × { 𝑟 } ) ) → 0 ∈ ℤ )
39		simpr	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 = ( ℤ × { 𝑟 } ) ) → 𝑝 = ( ℤ × { 𝑟 } ) )
40		opeq1	⊢ ( 𝑠 = 0 → ⟨ 𝑠 , 𝑟 ⟩ = ⟨ 0 , 𝑟 ⟩ )
41	40	eceq1d	⊢ ( 𝑠 = 0 → [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ = [ ⟨ 0 , 𝑟 ⟩ ] ∼ )
42	39 41	eqeqan12d	⊢ ( ( ( 𝑟 ∈ ℤ ∧ 𝑝 = ( ℤ × { 𝑟 } ) ) ∧ 𝑠 = 0 ) → ( 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ↔ ( ℤ × { 𝑟 } ) = [ ⟨ 0 , 𝑟 ⟩ ] ∼ ) )
43		0zd	⊢ ( 𝑟 ∈ ℤ → 0 ∈ ℤ )
44	1 2 3 4 5	pzriprnglem10	⊢ ( ( 0 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → [ ⟨ 0 , 𝑟 ⟩ ] ∼ = ( ℤ × { 𝑟 } ) )
45	43 44	mpancom	⊢ ( 𝑟 ∈ ℤ → [ ⟨ 0 , 𝑟 ⟩ ] ∼ = ( ℤ × { 𝑟 } ) )
46	45	eqcomd	⊢ ( 𝑟 ∈ ℤ → ( ℤ × { 𝑟 } ) = [ ⟨ 0 , 𝑟 ⟩ ] ∼ )
47	46	adantr	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 = ( ℤ × { 𝑟 } ) ) → ( ℤ × { 𝑟 } ) = [ ⟨ 0 , 𝑟 ⟩ ] ∼ )
48	38 42 47	rspcedvd	⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑝 = ( ℤ × { 𝑟 } ) ) → ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ )
49	48	ex	⊢ ( 𝑟 ∈ ℤ → ( 𝑝 = ( ℤ × { 𝑟 } ) → ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ) )
50	37 49	impbid	⊢ ( 𝑟 ∈ ℤ → ( ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ ↔ 𝑝 = ( ℤ × { 𝑟 } ) ) )
51	50	abbidv	⊢ ( 𝑟 ∈ ℤ → { 𝑝 ∣ ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { 𝑝 ∣ 𝑝 = ( ℤ × { 𝑟 } ) } )
52		iunsn	⊢ ∪ 𝑠 ∈ ℤ { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { 𝑝 ∣ ∃ 𝑠 ∈ ℤ 𝑝 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ }
53		df-sn	⊢ { ( ℤ × { 𝑟 } ) } = { 𝑝 ∣ 𝑝 = ( ℤ × { 𝑟 } ) }
54	51 52 53	3eqtr4g	⊢ ( 𝑟 ∈ ℤ → ∪ 𝑠 ∈ ℤ { [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { ( ℤ × { 𝑟 } ) } )
55	30 54	eqtrid	⊢ ( 𝑟 ∈ ℤ → ∪ 𝑠 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = { ( ℤ × { 𝑟 } ) } )
56	55	iuneq2i	⊢ ∪ 𝑟 ∈ ℤ ∪ 𝑠 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = ∪ 𝑟 ∈ ℤ { ( ℤ × { 𝑟 } ) }
57	26 56	eqtri	⊢ ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ { 𝑒 ∣ 𝑒 = [ ⟨ 𝑠 , 𝑟 ⟩ ] ∼ } = ∪ 𝑟 ∈ ℤ { ( ℤ × { 𝑟 } ) }
58	24 25 57	3eqtr3i	⊢ { 𝑒 ∣ ∃ 𝑝 ∈ ( ℤ × ℤ ) 𝑒 = [ 𝑝 ] ∼ } = ∪ 𝑟 ∈ ℤ { ( ℤ × { 𝑟 } ) }
59	7 17 58	3eqtr3i	⊢ ( Base ‘ 𝑄 ) = ∪ 𝑟 ∈ ℤ { ( ℤ × { 𝑟 } ) }