Step | Hyp | Ref
| Expression |
1 | | rnghmmul.x |
. . . 4
โข ๐ = (Baseโ๐
) |
2 | | rnghmmul.m |
. . . 4
โข ยท =
(.rโ๐
) |
3 | | rnghmmul.n |
. . . 4
โข ร =
(.rโ๐) |
4 | 1, 2, 3 | isrnghm 46264 |
. . 3
โข (๐น โ (๐
RngHomo ๐) โ ((๐
โ Rng โง ๐ โ Rng) โง (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) ร (๐นโ๐ฆ))))) |
5 | | fvoveq1 7385 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (๐นโ(๐ฅ ยท ๐ฆ)) = (๐นโ(๐ด ยท ๐ฆ))) |
6 | | fveq2 6847 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (๐นโ๐ฅ) = (๐นโ๐ด)) |
7 | 6 | oveq1d 7377 |
. . . . . . 7
โข (๐ฅ = ๐ด โ ((๐นโ๐ฅ) ร (๐นโ๐ฆ)) = ((๐นโ๐ด) ร (๐นโ๐ฆ))) |
8 | 5, 7 | eqeq12d 2753 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) ร (๐นโ๐ฆ)) โ (๐นโ(๐ด ยท ๐ฆ)) = ((๐นโ๐ด) ร (๐นโ๐ฆ)))) |
9 | | oveq2 7370 |
. . . . . . . 8
โข (๐ฆ = ๐ต โ (๐ด ยท ๐ฆ) = (๐ด ยท ๐ต)) |
10 | 9 | fveq2d 6851 |
. . . . . . 7
โข (๐ฆ = ๐ต โ (๐นโ(๐ด ยท ๐ฆ)) = (๐นโ(๐ด ยท ๐ต))) |
11 | | fveq2 6847 |
. . . . . . . 8
โข (๐ฆ = ๐ต โ (๐นโ๐ฆ) = (๐นโ๐ต)) |
12 | 11 | oveq2d 7378 |
. . . . . . 7
โข (๐ฆ = ๐ต โ ((๐นโ๐ด) ร (๐นโ๐ฆ)) = ((๐นโ๐ด) ร (๐นโ๐ต))) |
13 | 10, 12 | eqeq12d 2753 |
. . . . . 6
โข (๐ฆ = ๐ต โ ((๐นโ(๐ด ยท ๐ฆ)) = ((๐นโ๐ด) ร (๐นโ๐ฆ)) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต)))) |
14 | 8, 13 | rspc2va 3594 |
. . . . 5
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) ร (๐นโ๐ฆ))) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต))) |
15 | 14 | expcom 415 |
. . . 4
โข
(โ๐ฅ โ
๐ โ๐ฆ โ ๐ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) ร (๐นโ๐ฆ)) โ ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต)))) |
16 | 15 | ad2antll 728 |
. . 3
โข (((๐
โ Rng โง ๐ โ Rng) โง (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) ร (๐นโ๐ฆ)))) โ ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต)))) |
17 | 4, 16 | sylbi 216 |
. 2
โข (๐น โ (๐
RngHomo ๐) โ ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต)))) |
18 | 17 | 3impib 1117 |
1
โข ((๐น โ (๐
RngHomo ๐) โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐นโ(๐ด ยท ๐ต)) = ((๐นโ๐ด) ร (๐นโ๐ต))) |