Theorem qusaddf

Description: The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	qusaddf.u	|- ( ph -> U = ( R /s .~ ) )
	qusaddf.v	|- ( ph -> V = ( Base ` R ) )
	qusaddf.r	|- ( ph -> .~ Er V )
	qusaddf.z	|- ( ph -> R e. Z )
	qusaddf.e	|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
	qusaddf.c	|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
	qusaddf.p	|- .x. = ( +g ` R )
	qusaddf.a	|- .xb = ( +g ` U )
Assertion	qusaddf	|- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )

Proof

Step	Hyp	Ref	Expression
1		qusaddf.u	|- ( ph -> U = ( R /s .~ ) )
2		qusaddf.v	|- ( ph -> V = ( Base ` R ) )
3		qusaddf.r	|- ( ph -> .~ Er V )
4		qusaddf.z	|- ( ph -> R e. Z )
5		qusaddf.e	|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
6		qusaddf.c	|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
7		qusaddf.p	|- .x. = ( +g ` R )
8		qusaddf.a	|- .xb = ( +g ` U )
9		eqid	|- ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] .~ )
10		fvex	|- ( Base ` R ) e. _V
11	2 10	eqeltrdi	|- ( ph -> V e. _V )
12		erex	|- ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
13	3 11 12	sylc	|- ( ph -> .~ e. _V )
14	1 2 9 13 4	qusval	|- ( ph -> U = ( ( x e. V |-> [ x ] .~ ) "s R ) )
15	1 2 9 13 4	quslem	|- ( ph -> ( x e. V |-> [ x ] .~ ) : V -onto-> ( V /. .~ ) )
16	14 2 15 4 7 8	imasplusg	|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( ( x e. V |-> [ x ] .~ ) ` p ) , ( ( x e. V |-> [ x ] .~ ) ` q ) >. , ( ( x e. V |-> [ x ] .~ ) ` ( p .x. q ) ) >. } )
17	1 2 3 4 5 6 9 16	qusaddflem	|- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )