Step | Hyp | Ref
| Expression |
1 | | qusring2.u |
. . . 4
โข (๐ โ ๐ = (๐
/s โผ )) |
2 | | qusring2.v |
. . . 4
โข (๐ โ ๐ = (Baseโ๐
)) |
3 | | eqid 2733 |
. . . 4
โข (๐ข โ ๐ โฆ [๐ข] โผ ) = (๐ข โ ๐ โฆ [๐ข] โผ ) |
4 | | qusring2.r |
. . . . 5
โข (๐ โ โผ Er ๐) |
5 | | fvex 6859 |
. . . . . 6
โข
(Baseโ๐
)
โ V |
6 | 2, 5 | eqeltrdi 2842 |
. . . . 5
โข (๐ โ ๐ โ V) |
7 | | erex 8678 |
. . . . 5
โข ( โผ Er
๐ โ (๐ โ V โ โผ โ
V)) |
8 | 4, 6, 7 | sylc 65 |
. . . 4
โข (๐ โ โผ โ
V) |
9 | | qusring2.x |
. . . 4
โข (๐ โ ๐
โ Ring) |
10 | 1, 2, 3, 8, 9 | qusval 17432 |
. . 3
โข (๐ โ ๐ = ((๐ข โ ๐ โฆ [๐ข] โผ )
โs ๐
)) |
11 | | qusring2.p |
. . 3
โข + =
(+gโ๐
) |
12 | | qusring2.t |
. . 3
โข ยท =
(.rโ๐
) |
13 | | qusring2.o |
. . 3
โข 1 =
(1rโ๐
) |
14 | 1, 2, 3, 8, 9 | quslem 17433 |
. . 3
โข (๐ โ (๐ข โ ๐ โฆ [๐ข] โผ ):๐โontoโ(๐ / โผ )) |
15 | 9 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐
โ Ring) |
16 | | simprl 770 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฅ โ ๐) |
17 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ = (Baseโ๐
)) |
18 | 16, 17 | eleqtrd 2836 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฅ โ (Baseโ๐
)) |
19 | | simprr 772 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฆ โ ๐) |
20 | 19, 17 | eleqtrd 2836 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฆ โ (Baseโ๐
)) |
21 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐
) =
(Baseโ๐
) |
22 | 21, 11 | ringacl 20007 |
. . . . . 6
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ + ๐ฆ) โ (Baseโ๐
)) |
23 | 15, 18, 20, 22 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ + ๐ฆ) โ (Baseโ๐
)) |
24 | 23, 17 | eleqtrrd 2837 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ + ๐ฆ) โ ๐) |
25 | | qusring2.e1 |
. . . 4
โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ + ๐) โผ (๐ + ๐))) |
26 | 4, 6, 3, 24, 25 | ercpbl 17439 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) โง ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐)) โ ((๐ข โ ๐ โฆ [๐ข] โผ )โ(๐ + ๐)) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ(๐ + ๐)))) |
27 | 21, 12 | ringcl 19989 |
. . . . . 6
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ ยท ๐ฆ) โ (Baseโ๐
)) |
28 | 15, 18, 20, 27 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ (Baseโ๐
)) |
29 | 28, 17 | eleqtrrd 2837 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) |
30 | | qusring2.e2 |
. . . 4
โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ ยท ๐) โผ (๐ ยท ๐))) |
31 | 4, 6, 3, 29, 30 | ercpbl 17439 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) โง ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ๐)) โ ((๐ข โ ๐ โฆ [๐ข] โผ )โ(๐ ยท ๐)) = ((๐ข โ ๐ โฆ [๐ข] โผ )โ(๐ ยท ๐)))) |
32 | 10, 2, 11, 12, 13, 14, 26, 31, 9 | imasring 20053 |
. 2
โข (๐ โ (๐ โ Ring โง ((๐ข โ ๐ โฆ [๐ข] โผ )โ 1 ) =
(1rโ๐))) |
33 | 4, 6, 3 | divsfval 17437 |
. . . . 5
โข (๐ โ ((๐ข โ ๐ โฆ [๐ข] โผ )โ 1 ) = [ 1 ] โผ
) |
34 | 33 | eqcomd 2739 |
. . . 4
โข (๐ โ [ 1 ] โผ = ((๐ข โ ๐ โฆ [๐ข] โผ )โ 1
)) |
35 | 34 | eqeq1d 2735 |
. . 3
โข (๐ โ ([ 1 ] โผ =
(1rโ๐)
โ ((๐ข โ ๐ โฆ [๐ข] โผ )โ 1 ) =
(1rโ๐))) |
36 | 35 | anbi2d 630 |
. 2
โข (๐ โ ((๐ โ Ring โง [ 1 ] โผ =
(1rโ๐))
โ (๐ โ Ring โง
((๐ข โ ๐ โฆ [๐ข] โผ )โ 1 ) =
(1rโ๐)))) |
37 | 32, 36 | mpbird 257 |
1
โข (๐ โ (๐ โ Ring โง [ 1 ] โผ =
(1rโ๐))) |