Metamath Proof Explorer


Theorem qusmulval

Description: The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses qusaddf.u φ U = R / 𝑠 ˙
qusaddf.v φ V = Base R
qusaddf.r φ ˙ Er V
qusaddf.z φ R Z
qusaddf.e φ a ˙ p b ˙ q a · ˙ b ˙ p · ˙ q
qusaddf.c φ p V q V p · ˙ q V
qusmulf.p · ˙ = R
qusmulf.a ˙ = U
Assertion qusmulval φ X V Y V X ˙ ˙ Y ˙ = X · ˙ Y ˙

Proof

Step Hyp Ref Expression
1 qusaddf.u φ U = R / 𝑠 ˙
2 qusaddf.v φ V = Base R
3 qusaddf.r φ ˙ Er V
4 qusaddf.z φ R Z
5 qusaddf.e φ a ˙ p b ˙ q a · ˙ b ˙ p · ˙ q
6 qusaddf.c φ p V q V p · ˙ q V
7 qusmulf.p · ˙ = R
8 qusmulf.a ˙ = U
9 eqid x V x ˙ = x V x ˙
10 fvex Base R V
11 2 10 eqeltrdi φ V V
12 erex ˙ Er V V V ˙ V
13 3 11 12 sylc φ ˙ V
14 1 2 9 13 4 qusval φ U = x V x ˙ 𝑠 R
15 1 2 9 13 4 quslem φ x V x ˙ : V onto V / ˙
16 14 2 15 4 7 8 imasmulr φ ˙ = p V q V x V x ˙ p x V x ˙ q x V x ˙ p · ˙ q
17 1 2 3 4 5 6 9 16 qusaddvallem φ X V Y V X ˙ ˙ Y ˙ = X · ˙ Y ˙