Step | Hyp | Ref
| Expression |
1 | | df-rnghomo 46259 |
. . 3
โข RngHomo
= (๐ โ Rng, ๐ โ Rng โฆ
โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
2 | 1 | a1i 11 |
. 2
โข ((๐
โ Rng โง ๐ โ Rng) โ RngHomo =
(๐ โ Rng, ๐ โ Rng โฆ
โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))})) |
3 | | fveq2 6847 |
. . . . . . 7
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
4 | | isrnghm.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . 6
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
6 | 5 | csbeq1d 3864 |
. . . . 5
โข (๐ = ๐
โ โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = โฆ๐ต / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
7 | | fveq2 6847 |
. . . . . . . 8
โข (๐ = ๐ โ (Baseโ๐ ) = (Baseโ๐)) |
8 | | rnghmval.c |
. . . . . . . 8
โข ๐ถ = (Baseโ๐) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . 7
โข (๐ = ๐ โ (Baseโ๐ ) = ๐ถ) |
10 | 9 | csbeq1d 3864 |
. . . . . 6
โข (๐ = ๐ โ โฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = โฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
11 | 10 | csbeq2dv 3867 |
. . . . 5
โข (๐ = ๐ โ โฆ๐ต / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = โฆ๐ต / ๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
12 | 6, 11 | sylan9eq 2797 |
. . . 4
โข ((๐ = ๐
โง ๐ = ๐) โ โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = โฆ๐ต / ๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
13 | 12 | adantl 483 |
. . 3
โข (((๐
โ Rng โง ๐ โ Rng) โง (๐ = ๐
โง ๐ = ๐)) โ โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = โฆ๐ต / ๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
14 | 4 | fvexi 6861 |
. . . . . 6
โข ๐ต โ V |
15 | 8 | fvexi 6861 |
. . . . . 6
โข ๐ถ โ V |
16 | | oveq12 7371 |
. . . . . . . 8
โข ((๐ค = ๐ถ โง ๐ฃ = ๐ต) โ (๐ค โm ๐ฃ) = (๐ถ โm ๐ต)) |
17 | 16 | ancoms 460 |
. . . . . . 7
โข ((๐ฃ = ๐ต โง ๐ค = ๐ถ) โ (๐ค โm ๐ฃ) = (๐ถ โm ๐ต)) |
18 | | raleq 3312 |
. . . . . . . . 9
โข (๐ฃ = ๐ต โ (โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))) โ โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))))) |
19 | 18 | raleqbi1dv 3310 |
. . . . . . . 8
โข (๐ฃ = ๐ต โ (โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))))) |
20 | 19 | adantr 482 |
. . . . . . 7
โข ((๐ฃ = ๐ต โง ๐ค = ๐ถ) โ (โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))))) |
21 | 17, 20 | rabeqbidv 3427 |
. . . . . 6
โข ((๐ฃ = ๐ต โง ๐ค = ๐ถ) โ {๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))}) |
22 | 14, 15, 21 | csbie2 3902 |
. . . . 5
โข
โฆ๐ต /
๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} |
23 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐
โ (+gโ๐) = (+gโ๐
)) |
24 | | rnghmval.p |
. . . . . . . . . . . 12
โข + =
(+gโ๐
) |
25 | 23, 24 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ = ๐
โ (+gโ๐) = + ) |
26 | 25 | oveqdr 7390 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ (๐ฅ(+gโ๐)๐ฆ) = (๐ฅ + ๐ฆ)) |
27 | 26 | fveq2d 6851 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ (๐โ(๐ฅ(+gโ๐)๐ฆ)) = (๐โ(๐ฅ + ๐ฆ))) |
28 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (+gโ๐ ) = (+gโ๐)) |
29 | | rnghmval.a |
. . . . . . . . . . . 12
โข โ =
(+gโ๐) |
30 | 28, 29 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (+gโ๐ ) = โ ) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ (+gโ๐ ) = โ ) |
32 | 31 | oveqd 7379 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))) |
33 | 27, 32 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐ = ๐
โง ๐ = ๐) โ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โ (๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))) |
34 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
35 | | isrnghm.t |
. . . . . . . . . . . 12
โข ยท =
(.rโ๐
) |
36 | 34, 35 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ = ๐
โ (.rโ๐) = ยท ) |
37 | 36 | oveqdr 7390 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ (๐ฅ(.rโ๐)๐ฆ) = (๐ฅ ยท ๐ฆ)) |
38 | 37 | fveq2d 6851 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ (๐โ(๐ฅ(.rโ๐)๐ฆ)) = (๐โ(๐ฅ ยท ๐ฆ))) |
39 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (.rโ๐ ) = (.rโ๐)) |
40 | | isrnghm.m |
. . . . . . . . . . . 12
โข โ =
(.rโ๐) |
41 | 39, 40 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (.rโ๐ ) = โ ) |
42 | 41 | adantl 483 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ (.rโ๐ ) = โ ) |
43 | 42 | oveqd 7379 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))) |
44 | 38, 43 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐ = ๐
โง ๐ = ๐) โ ((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)) โ (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))) |
45 | 33, 44 | anbi12d 632 |
. . . . . . 7
โข ((๐ = ๐
โง ๐ = ๐) โ (((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))) โ ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))))) |
46 | 45 | 2ralbidv 3213 |
. . . . . 6
โข ((๐ = ๐
โง ๐ = ๐) โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))))) |
47 | 46 | rabbidv 3418 |
. . . . 5
โข ((๐ = ๐
โง ๐ = ๐) โ {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |
48 | 22, 47 | eqtrid 2789 |
. . . 4
โข ((๐ = ๐
โง ๐ = ๐) โ โฆ๐ต / ๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |
49 | 48 | adantl 483 |
. . 3
โข (((๐
โ Rng โง ๐ โ Rng) โง (๐ = ๐
โง ๐ = ๐)) โ โฆ๐ต / ๐ฃโฆโฆ๐ถ / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |
50 | 13, 49 | eqtrd 2777 |
. 2
โข (((๐
โ Rng โง ๐ โ Rng) โง (๐ = ๐
โง ๐ = ๐)) โ โฆ(Baseโ๐) / ๐ฃโฆโฆ(Baseโ๐ ) / ๐คโฆ{๐ โ (๐ค โm ๐ฃ) โฃ โ๐ฅ โ ๐ฃ โ๐ฆ โ ๐ฃ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ )(๐โ๐ฆ)) โง (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐ )(๐โ๐ฆ)))} = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |
51 | | simpl 484 |
. 2
โข ((๐
โ Rng โง ๐ โ Rng) โ ๐
โ Rng) |
52 | | simpr 486 |
. 2
โข ((๐
โ Rng โง ๐ โ Rng) โ ๐ โ Rng) |
53 | | ovex 7395 |
. . . 4
โข (๐ถ โm ๐ต) โ V |
54 | 53 | rabex 5294 |
. . 3
โข {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))} โ V |
55 | 54 | a1i 11 |
. 2
โข ((๐
โ Rng โง ๐ โ Rng) โ {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))} โ V) |
56 | 2, 50, 51, 52, 55 | ovmpod 7512 |
1
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐
RngHomo ๐) = {๐ โ (๐ถ โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ + ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |