Metamath Proof Explorer


Theorem qusmulf

Description: The base set of an image 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 ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
qusmulf.p · = ( .r𝑅 )
qusmulf.a = ( .r𝑈 )
Assertion qusmulf ( 𝜑 : ( ( 𝑉 / ) × ( 𝑉 / ) ) ⟶ ( 𝑉 / ) )

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 qusmulf.p · = ( .r𝑅 )
8 qusmulf.a = ( .r𝑈 )
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 imasmulr ( 𝜑 = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( ( 𝑥𝑉 ↦ [ 𝑥 ] ) ‘ 𝑝 ) , ( ( 𝑥𝑉 ↦ [ 𝑥 ] ) ‘ 𝑞 ) ⟩ , ( ( 𝑥𝑉 ↦ [ 𝑥 ] ) ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
17 1 2 3 4 5 6 9 16 qusaddflem ( 𝜑 : ( ( 𝑉 / ) × ( 𝑉 / ) ) ⟶ ( 𝑉 / ) )