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