eroprf

Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	eropr.1	⊢ 𝐽 = ( 𝐴 / 𝑅 )
	eropr.2	⊢ 𝐾 = ( 𝐵 / 𝑆 )
	eropr.3	⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
	eropr.4	⊢ ( 𝜑 → 𝑅 Er 𝑈 )
	eropr.5	⊢ ( 𝜑 → 𝑆 Er 𝑉 )
	eropr.6	⊢ ( 𝜑 → 𝑇 Er 𝑊 )
	eropr.7	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
	eropr.8	⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
	eropr.9	⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
	eropr.10	⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
	eropr.11	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
	eropr.12	⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
	eropr.13	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	eropr.14	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
	eropr.15	⊢ 𝐿 = ( 𝐶 / 𝑇 )
Assertion	eroprf	⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐾 ) ⟶ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		eropr.1	⊢ 𝐽 = ( 𝐴 / 𝑅 )
2		eropr.2	⊢ 𝐾 = ( 𝐵 / 𝑆 )
3		eropr.3	⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
4		eropr.4	⊢ ( 𝜑 → 𝑅 Er 𝑈 )
5		eropr.5	⊢ ( 𝜑 → 𝑆 Er 𝑉 )
6		eropr.6	⊢ ( 𝜑 → 𝑇 Er 𝑊 )
7		eropr.7	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
8		eropr.8	⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
9		eropr.9	⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
10		eropr.10	⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
11		eropr.11	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
12		eropr.12	⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
13		eropr.13	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
14		eropr.14	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
15		eropr.15	⊢ 𝐿 = ( 𝐶 / 𝑇 )
16	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → 𝑇 ∈ 𝑍 )
17	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
18	17	fovcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝐶 )
19		ecelqsw	⊢ ( ( 𝑇 ∈ 𝑍 ∧ ( 𝑝 + 𝑞 ) ∈ 𝐶 ) → [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ ( 𝐶 / 𝑇 ) )
20	16 18 19	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ ( 𝐶 / 𝑇 ) )
21	20 15	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ 𝐿 )
22		eleq1a	⊢ ( [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ 𝐿 → ( 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 → 𝑧 ∈ 𝐿 ) )
23	21 22	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 → 𝑧 ∈ 𝐿 ) )
24	23	adantld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → 𝑧 ∈ 𝐿 ) )
25	24	rexlimdvva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → 𝑧 ∈ 𝐿 ) )
26	25	abssdv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) } ⊆ 𝐿 )
27	1 2 3 4 5 6 7 8 9 10 11	eroveu	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
28		iotacl	⊢ ( ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) } )
29	27 28	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) } )
30	26 29	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ 𝐿 )
31	30	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐾 ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ 𝐿 )
32		eqid	⊢ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
33	32	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐾 ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ 𝐿 ↔ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) : ( 𝐽 × 𝐾 ) ⟶ 𝐿 )
34	31 33	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) : ( 𝐽 × 𝐾 ) ⟶ 𝐿 )
35	1 2 3 4 5 6 7 8 9 10 11 12	erovlem	⊢ ( 𝜑 → ⨣ = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
36	35	feq1d	⊢ ( 𝜑 → ( ⨣ : ( 𝐽 × 𝐾 ) ⟶ 𝐿 ↔ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) : ( 𝐽 × 𝐾 ) ⟶ 𝐿 ) )
37	34 36	mpbird	⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐾 ) ⟶ 𝐿 )

Metamath Proof Explorer

Theorem eroprf

Proof