Theorem qqhvq

Description: The image of a quotient by the QQHom homomorphism. (Contributed by Thierry Arnoux, 28-Oct-2017)

	Ref	Expression
Hypotheses	qqhval2.0	|- B = ( Base ` R )
	qqhval2.1	|- ./ = ( /r ` R )
	qqhval2.2	|- L = ( ZRHom ` R )
Assertion	qqhvq	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( QQHom ` R ) ` ( X / Y ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	|- B = ( Base ` R )
2		qqhval2.1	|- ./ = ( /r ` R )
3		qqhval2.2	|- L = ( ZRHom ` R )
4		zssq	|- ZZ C_ QQ
5		simpr1	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> X e. ZZ )
6	4 5	sseldi	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> X e. QQ )
7		simpr2	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y e. ZZ )
8	4 7	sseldi	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y e. QQ )
9		simpr3	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y =/= 0 )
10		qdivcl	|- ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( X / Y ) e. QQ )
11	6 8 9 10	syl3anc	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X / Y ) e. QQ )
12	1 2 3	qqhvval	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X / Y ) e. QQ ) -> ( ( QQHom ` R ) ` ( X / Y ) ) = ( ( L ` ( numer ` ( X / Y ) ) ) ./ ( L ` ( denom ` ( X / Y ) ) ) ) )
13	11 12	syldan	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( QQHom ` R ) ` ( X / Y ) ) = ( ( L ` ( numer ` ( X / Y ) ) ) ./ ( L ` ( denom ` ( X / Y ) ) ) ) )
14	1 2 3	qqhval2lem	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( numer ` ( X / Y ) ) ) ./ ( L ` ( denom ` ( X / Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )
15	13 14	eqtrd	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( QQHom ` R ) ` ( X / Y ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )