Step | Hyp | Ref
| Expression |
1 | | fvexd 6857 |
. . 3
โข (๐ = ๐
โ (Baseโ๐) โ V) |
2 | | fveq2 6842 |
. . . 4
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
3 | | isdomn.b |
. . . 4
โข ๐ต = (Baseโ๐
) |
4 | 2, 3 | eqtr4di 2794 |
. . 3
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
5 | | fvexd 6857 |
. . . 4
โข ((๐ = ๐
โง ๐ = ๐ต) โ (0gโ๐) โ V) |
6 | | fveq2 6842 |
. . . . . 6
โข (๐ = ๐
โ (0gโ๐) = (0gโ๐
)) |
7 | 6 | adantr 481 |
. . . . 5
โข ((๐ = ๐
โง ๐ = ๐ต) โ (0gโ๐) = (0gโ๐
)) |
8 | | isdomn.z |
. . . . 5
โข 0 =
(0gโ๐
) |
9 | 7, 8 | eqtr4di 2794 |
. . . 4
โข ((๐ = ๐
โง ๐ = ๐ต) โ (0gโ๐) = 0 ) |
10 | | simplr 767 |
. . . . 5
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ ๐ = ๐ต) |
11 | | fveq2 6842 |
. . . . . . . . . 10
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
12 | | isdomn.t |
. . . . . . . . . 10
โข ยท =
(.rโ๐
) |
13 | 11, 12 | eqtr4di 2794 |
. . . . . . . . 9
โข (๐ = ๐
โ (.rโ๐) = ยท ) |
14 | 13 | oveqdr 7385 |
. . . . . . . 8
โข ((๐ = ๐
โง ๐ = ๐ต) โ (๐ฅ(.rโ๐)๐ฆ) = (๐ฅ ยท ๐ฆ)) |
15 | | id 22 |
. . . . . . . 8
โข (๐ง = 0 โ ๐ง = 0 ) |
16 | 14, 15 | eqeqan12d 2750 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ ยท ๐ฆ) = 0 )) |
17 | | eqeq2 2748 |
. . . . . . . . 9
โข (๐ง = 0 โ (๐ฅ = ๐ง โ ๐ฅ = 0 )) |
18 | | eqeq2 2748 |
. . . . . . . . 9
โข (๐ง = 0 โ (๐ฆ = ๐ง โ ๐ฆ = 0 )) |
19 | 17, 18 | orbi12d 917 |
. . . . . . . 8
โข (๐ง = 0 โ ((๐ฅ = ๐ง โจ ๐ฆ = ๐ง) โ (๐ฅ = 0 โจ ๐ฆ = 0 ))) |
20 | 19 | adantl 482 |
. . . . . . 7
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ ((๐ฅ = ๐ง โจ ๐ฆ = ๐ง) โ (๐ฅ = 0 โจ ๐ฆ = 0 ))) |
21 | 16, 20 | imbi12d 344 |
. . . . . 6
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ (((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง)) โ ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
22 | 10, 21 | raleqbidv 3319 |
. . . . 5
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ (โ๐ฆ โ ๐ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง)) โ โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
23 | 10, 22 | raleqbidv 3319 |
. . . 4
โข (((๐ = ๐
โง ๐ = ๐ต) โง ๐ง = 0 ) โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
24 | 5, 9, 23 | sbcied2 3786 |
. . 3
โข ((๐ = ๐
โง ๐ = ๐ต) โ ([(0gโ๐) / ๐ง]โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
25 | 1, 4, 24 | sbcied2 3786 |
. 2
โข (๐ = ๐
โ ([(Baseโ๐) / ๐][(0gโ๐) / ๐ง]โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |
26 | | df-domn 20754 |
. 2
โข Domn =
{๐ โ NzRing โฃ
[(Baseโ๐) /
๐][(0gโ๐) / ๐ง]โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ(.rโ๐)๐ฆ) = ๐ง โ (๐ฅ = ๐ง โจ ๐ฆ = ๐ง))} |
27 | 25, 26 | elrab2 3648 |
1
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = 0 โ (๐ฅ = 0 โจ ๐ฆ = 0 )))) |