Theorem eroprf2

Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	eropr2.1	⊢ 𝐽 = ( 𝐴 / ∼ )
	eropr2.2	⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑥 = [ 𝑝 ] ∼ ∧ 𝑦 = [ 𝑞 ] ∼ ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] ∼ ) }
	eropr2.3	⊢ ( 𝜑 → ∼ ∈ 𝑋 )
	eropr2.4	⊢ ( 𝜑 → ∼ Er 𝑈 )
	eropr2.5	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
	eropr2.6	⊢ ( 𝜑 → + : ( 𝐴 × 𝐴 ) ⟶ 𝐴 )
	eropr2.7	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) ) → ( ( 𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢 ) → ( 𝑟 + 𝑡 ) ∼ ( 𝑠 + 𝑢 ) ) )
Assertion	eroprf2	⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐽 ) ⟶ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		eropr2.1	⊢ 𝐽 = ( 𝐴 / ∼ )
2		eropr2.2	⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑥 = [ 𝑝 ] ∼ ∧ 𝑦 = [ 𝑞 ] ∼ ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] ∼ ) }
3		eropr2.3	⊢ ( 𝜑 → ∼ ∈ 𝑋 )
4		eropr2.4	⊢ ( 𝜑 → ∼ Er 𝑈 )
5		eropr2.5	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
6		eropr2.6	⊢ ( 𝜑 → + : ( 𝐴 × 𝐴 ) ⟶ 𝐴 )
7		eropr2.7	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) ) → ( ( 𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢 ) → ( 𝑟 + 𝑡 ) ∼ ( 𝑠 + 𝑢 ) ) )
8	1 1 3 4 4 4 5 5 5 6 7 2 3 3 1	eroprf	⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐽 ) ⟶ 𝐽 )