Metamath Proof Explorer


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 ( 𝜑 : ( 𝐽 × 𝐽 ) ⟶ 𝐽 )