This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusaddf

Description: The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses qusaddf.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
qusaddf.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
qusaddf.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
qusaddf.z ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
qusaddf.e ⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
qusaddf.c ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
qusaddf.p ⊢ · = ( +g ‘ 𝑅 )
qusaddf.a ⊢ ∙ = ( +g ‘ 𝑈 )
Assertion qusaddf ( 𝜑 → ∙ : ( ( 𝑉 / ∼ ) × ( 𝑉 / ∼ ) ) ⟶ ( 𝑉 / ∼ ) )

Proof

Step Hyp Ref Expression
1 qusaddf.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2 qusaddf.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 qusaddf.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
4 qusaddf.z ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 qusaddf.e ⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) )
6 qusaddf.c ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
7 qusaddf.p ⊢ · = ( +g ‘ 𝑅 )
8 qusaddf.a ⊢ ∙ = ( +g ‘ 𝑈 )
9 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
10 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
11 2 10 eqeltrdi ⊢ ( 𝜑 → 𝑉 ∈ V )
12 erex ⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
13 3 11 12 sylc ⊢ ( 𝜑 → ∼ ∈ V )
14 1 2 9 13 4 qusval ⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) )
15 1 2 9 13 4 quslem ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) )
16 14 2 15 4 7 8 imasplusg ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑝 ) , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑞 ) ⟩ , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
17 1 2 3 4 5 6 9 16 qusaddflem ⊢ ( 𝜑 → ∙ : ( ( 𝑉 / ∼ ) × ( 𝑉 / ∼ ) ) ⟶ ( 𝑉 / ∼ ) )