Step |
Hyp |
Ref |
Expression |
1 |
|
rhmdvd.u |
|- U = ( Unit ` S ) |
2 |
|
rhmdvd.x |
|- X = ( Base ` R ) |
3 |
|
rhmdvd.d |
|- ./ = ( /r ` S ) |
4 |
|
rhmdvd.m |
|- .x. = ( .r ` R ) |
5 |
|
simp1 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> F e. ( R RingHom S ) ) |
6 |
|
simp21 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> A e. X ) |
7 |
|
simp23 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> C e. X ) |
8 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
9 |
2 4 8
|
rhmmul |
|- ( ( F e. ( R RingHom S ) /\ A e. X /\ C e. X ) -> ( F ` ( A .x. C ) ) = ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ) |
10 |
5 6 7 9
|
syl3anc |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` ( A .x. C ) ) = ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ) |
11 |
|
simp22 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> B e. X ) |
12 |
2 4 8
|
rhmmul |
|- ( ( F e. ( R RingHom S ) /\ B e. X /\ C e. X ) -> ( F ` ( B .x. C ) ) = ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) |
13 |
5 11 7 12
|
syl3anc |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` ( B .x. C ) ) = ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) |
14 |
10 13
|
oveq12d |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) = ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) ) |
15 |
|
rhmrcl2 |
|- ( F e. ( R RingHom S ) -> S e. Ring ) |
16 |
15
|
3ad2ant1 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> S e. Ring ) |
17 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
18 |
2 17
|
rhmf |
|- ( F e. ( R RingHom S ) -> F : X --> ( Base ` S ) ) |
19 |
18
|
3ad2ant1 |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> F : X --> ( Base ` S ) ) |
20 |
19 6
|
ffvelrnd |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` A ) e. ( Base ` S ) ) |
21 |
|
simp3l |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` B ) e. U ) |
22 |
|
simp3r |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` C ) e. U ) |
23 |
17 1 3 8
|
dvrcan5 |
|- ( ( S e. Ring /\ ( ( F ` A ) e. ( Base ` S ) /\ ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) = ( ( F ` A ) ./ ( F ` B ) ) ) |
24 |
16 20 21 22 23
|
syl13anc |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) = ( ( F ` A ) ./ ( F ` B ) ) ) |
25 |
14 24
|
eqtr2d |
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` A ) ./ ( F ` B ) ) = ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) ) |