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 φU=R/𝑠˙
qusaddf.v φV=BaseR
qusaddf.r φ˙ErV
qusaddf.z φRZ
qusaddf.e φa˙pb˙qa·˙b˙p·˙q
qusaddf.c φpVqVp·˙qV
qusaddflem.f F=xVx˙
qusaddflem.g φ˙=pVqVFpFqFp·˙q
Assertion qusaddflem φ˙:V/˙×V/˙V/˙

Proof

Step Hyp Ref Expression
1 qusaddf.u φU=R/𝑠˙
2 qusaddf.v φV=BaseR
3 qusaddf.r φ˙ErV
4 qusaddf.z φRZ
5 qusaddf.e φa˙pb˙qa·˙b˙p·˙q
6 qusaddf.c φpVqVp·˙qV
7 qusaddflem.f F=xVx˙
8 qusaddflem.g φ˙=pVqVFpFqFp·˙q
9 fvex BaseRV
10 2 9 eqeltrdi φVV
11 erex ˙ErVVV˙V
12 3 10 11 sylc φ˙V
13 1 2 7 12 4 quslem φF:VontoV/˙
14 3 10 7 6 5 ercpbl φaVbVpVqVFa=FpFb=FqFa·˙b=Fp·˙q
15 13 14 8 6 imasaddflem φ˙:V/˙×V/˙V/˙