Metamath Proof Explorer


Theorem qusaddflem

Description: The operation of a quotient structure is 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 ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
qusaddflem.f 𝐹 = ( 𝑥𝑉 ↦ [ 𝑥 ] )
qusaddflem.g ( 𝜑 = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
Assertion qusaddflem ( 𝜑 : ( ( 𝑉 / ) × ( 𝑉 / ) ) ⟶ ( 𝑉 / ) )

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 qusaddflem.f 𝐹 = ( 𝑥𝑉 ↦ [ 𝑥 ] )
8 qusaddflem.g ( 𝜑 = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
9 fvex ( Base ‘ 𝑅 ) ∈ V
10 2 9 eqeltrdi ( 𝜑𝑉 ∈ V )
11 erex ( Er 𝑉 → ( 𝑉 ∈ V → ∈ V ) )
12 3 10 11 sylc ( 𝜑 ∈ V )
13 1 2 7 12 4 quslem ( 𝜑𝐹 : 𝑉onto→ ( 𝑉 / ) )
14 3 10 7 6 5 ercpbl ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
15 13 14 8 6 imasaddflem ( 𝜑 : ( ( 𝑉 / ) × ( 𝑉 / ) ) ⟶ ( 𝑉 / ) )