Metamath Proof Explorer


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 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( ( 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 ) ) )