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=BaseR
qqhval2.1 ×˙=/rR
qqhval2.2 L=ℤRHomR
Assertion qqhvq RDivRingchrR=0XYY0ℚHomRXY=LX×˙LY

Proof

Step Hyp Ref Expression
1 qqhval2.0 B=BaseR
2 qqhval2.1 ×˙=/rR
3 qqhval2.2 L=ℤRHomR
4 zssq
5 simpr1 RDivRingchrR=0XYY0X
6 4 5 sselid RDivRingchrR=0XYY0X
7 simpr2 RDivRingchrR=0XYY0Y
8 4 7 sselid RDivRingchrR=0XYY0Y
9 simpr3 RDivRingchrR=0XYY0Y0
10 qdivcl XYY0XY
11 6 8 9 10 syl3anc RDivRingchrR=0XYY0XY
12 1 2 3 qqhvval RDivRingchrR=0XYℚHomRXY=LnumerXY×˙LdenomXY
13 11 12 syldan RDivRingchrR=0XYY0ℚHomRXY=LnumerXY×˙LdenomXY
14 1 2 3 qqhval2lem RDivRingchrR=0XYY0LnumerXY×˙LdenomXY=LX×˙LY
15 13 14 eqtrd RDivRingchrR=0XYY0ℚHomRXY=LX×˙LY