Metamath Proof Explorer

Theorem 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 ecelqsg ⊢ ( ( 𝑇 ∈ 𝑍 ∧ ( 𝑝 + 𝑞 ) ∈ 𝐶 ) → [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ ( 𝐶 / 𝑇 ) )
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 ⊢ ( 𝜑 → ⨣ : ( 𝐽 × 𝐾 ) ⟶ 𝐿 )