Metamath Proof Explorer

Theorem qusaddvallem

Description: Value of an operation defined on a quotient structure. (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 qusaddvallem ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )

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 imasaddvallem ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
16 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ∼ Er 𝑉 )
17 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑉 ∈ V )
18 16 17 7 divsfval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) = [ 𝑋 ] ∼ )
19 16 17 7 divsfval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑌 ) = [ 𝑌 ] ∼ )
20 18 19 oveq12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) )
21 16 17 7 divsfval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = [ ( 𝑋 · 𝑌 ) ] ∼ )
22 15 20 21 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )