Theorem qqhvval

Description: Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 30-Oct-2017)

	Ref	Expression
Hypotheses	qqhval2.0	|- B = ( Base ` R )
	qqhval2.1	|- ./ = ( /r ` R )
	qqhval2.2	|- L = ( ZRHom ` R )
Assertion	qqhvval	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( QQHom ` R ) ` Q ) = ( ( L ` ( numer ` Q ) ) ./ ( L ` ( denom ` Q ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	|- B = ( Base ` R )
2		qqhval2.1	|- ./ = ( /r ` R )
3		qqhval2.2	|- L = ( ZRHom ` R )
4	1 2 3	qqhval2	|- ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) = ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) )
5	4	adantr	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( QQHom ` R ) = ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) )
6		simpr	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> q = Q )
7	6	fveq2d	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> ( numer ` q ) = ( numer ` Q ) )
8	7	fveq2d	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> ( L ` ( numer ` q ) ) = ( L ` ( numer ` Q ) ) )
9	6	fveq2d	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> ( denom ` q ) = ( denom ` Q ) )
10	9	fveq2d	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> ( L ` ( denom ` q ) ) = ( L ` ( denom ` Q ) ) )
11	8 10	oveq12d	|- ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) /\ q = Q ) -> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) = ( ( L ` ( numer ` Q ) ) ./ ( L ` ( denom ` Q ) ) ) )
12		simpr	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> Q e. QQ )
13		ovexd	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( L ` ( numer ` Q ) ) ./ ( L ` ( denom ` Q ) ) ) e. _V )
14	5 11 12 13	fvmptd	|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( QQHom ` R ) ` Q ) = ( ( L ` ( numer ` Q ) ) ./ ( L ` ( denom ` Q ) ) ) )