Theorem qusaddflem

Description: The operation of a quotient structure is 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 )
	qusaddflem.f	|- F = ( x e. V |-> [ x ] .~ )
	qusaddflem.g	|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Assertion	qusaddflem	|- ( 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		qusaddflem.f	|- F = ( x e. V |-> [ x ] .~ )
8		qusaddflem.g	|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
9		fvex	|- ( Base ` R ) e. _V
10	2 9	eqeltrdi	|- ( ph -> V e. _V )
11		erex	|- ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
12	3 10 11	sylc	|- ( ph -> .~ e. _V )
13	1 2 7 12 4	quslem	|- ( ph -> F : V -onto-> ( V /. .~ ) )
14	3 10 7 6 5	ercpbl	|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
15	13 14 8 6	imasaddflem	|- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )