Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
(Baseโ๐
) =
(Baseโ๐
) |
2 | | eqid 2733 |
. . 3
โข
(.rโ๐
) = (.rโ๐
) |
3 | | eqid 2733 |
. . 3
โข
(1rโ๐
) = (1rโ๐
) |
4 | 1, 2, 3 | dfur2 20007 |
. 2
โข
(1rโ๐
) = (โฉ๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) |
5 | | ringurd.z |
. . . 4
โข (๐ โ 1 โ ๐ต) |
6 | | ringurd.b |
. . . 4
โข (๐ โ ๐ต = (Baseโ๐
)) |
7 | 5, 6 | eleqtrd 2836 |
. . 3
โข (๐ โ 1 โ (Baseโ๐
)) |
8 | | ringurd.i |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
9 | | ringurd.j |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ ยท 1 ) = ๐ฅ) |
10 | 8, 9 | jca 513 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต) โ (( 1 ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท 1 ) = ๐ฅ)) |
11 | 10 | ralrimiva 3147 |
. . . 4
โข (๐ โ โ๐ฅ โ ๐ต (( 1 ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท 1 ) = ๐ฅ)) |
12 | | ringurd.p |
. . . . . . . . 9
โข (๐ โ ยท =
(.rโ๐
)) |
13 | 12 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต) โ ยท =
(.rโ๐
)) |
14 | 13 | oveqd 7426 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ต) โ ( 1 ยท ๐ฅ) = ( 1 (.rโ๐
)๐ฅ)) |
15 | 14 | eqeq1d 2735 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ (( 1 ยท ๐ฅ) = ๐ฅ โ ( 1 (.rโ๐
)๐ฅ) = ๐ฅ)) |
16 | 13 | oveqd 7426 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ ยท 1 ) = (๐ฅ(.rโ๐
) 1 )) |
17 | 16 | eqeq1d 2735 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท 1 ) = ๐ฅ โ (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)) |
18 | 15, 17 | anbi12d 632 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต) โ ((( 1 ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท 1 ) = ๐ฅ) โ (( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ))) |
19 | 6, 18 | raleqbidva 3328 |
. . . 4
โข (๐ โ (โ๐ฅ โ ๐ต (( 1 ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท 1 ) = ๐ฅ) โ โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ))) |
20 | 11, 19 | mpbid 231 |
. . 3
โข (๐ โ โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)) |
21 | 6 | eleq2d 2820 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ต โ ๐ โ (Baseโ๐
))) |
22 | 13 | oveqd 7426 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ ยท ๐ฅ) = (๐(.rโ๐
)๐ฅ)) |
23 | 22 | eqeq1d 2735 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐ ยท ๐ฅ) = ๐ฅ โ (๐(.rโ๐
)๐ฅ) = ๐ฅ)) |
24 | 13 | oveqd 7426 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ ยท ๐) = (๐ฅ(.rโ๐
)๐)) |
25 | 24 | eqeq1d 2735 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท ๐) = ๐ฅ โ (๐ฅ(.rโ๐
)๐) = ๐ฅ)) |
26 | 23, 25 | anbi12d 632 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต) โ (((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ) โ ((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) |
27 | 6, 26 | raleqbidva 3328 |
. . . . . . . 8
โข (๐ โ (โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ) โ โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) |
28 | 21, 27 | anbi12d 632 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) โ (๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ)))) |
29 | 8 | ralrimiva 3147 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ฅ โ ๐ต ( 1 ยท ๐ฅ) = ๐ฅ) |
30 | 29 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ โ๐ฅ โ ๐ต ( 1 ยท ๐ฅ) = ๐ฅ) |
31 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
32 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง ๐ฅ = ๐) โ ๐ฅ = ๐) |
33 | 32 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง ๐ฅ = ๐) โ ( 1 ยท ๐ฅ) = ( 1 ยท ๐)) |
34 | 33, 32 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง ๐ฅ = ๐) โ (( 1 ยท ๐ฅ) = ๐ฅ โ ( 1 ยท ๐) = ๐)) |
35 | 31, 34 | rspcdv 3605 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (โ๐ฅ โ ๐ต ( 1 ยท ๐ฅ) = ๐ฅ โ ( 1 ยท ๐) = ๐)) |
36 | 30, 35 | mpd 15 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ( 1 ยท ๐) = ๐) |
37 | 36 | adantrr 716 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) โ ( 1 ยท ๐) = ๐) |
38 | 5 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) โ 1 โ ๐ต) |
39 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) โ โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) |
40 | | oveq2 7417 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (๐ ยท ๐ฅ) = (๐ ยท 1 )) |
41 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ ๐ฅ = 1 ) |
42 | 40, 41 | eqeq12d 2749 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ ((๐ ยท ๐ฅ) = ๐ฅ โ (๐ ยท 1 ) = 1 )) |
43 | | oveq1 7416 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (๐ฅ ยท ๐) = ( 1 ยท ๐)) |
44 | 43, 41 | eqeq12d 2749 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ ((๐ฅ ยท ๐) = ๐ฅ โ ( 1 ยท ๐) = 1 )) |
45 | 42, 44 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ) โ ((๐ ยท 1 ) = 1 โง ( 1 ยท ๐) = 1 ))) |
46 | 45 | rspcva 3611 |
. . . . . . . . . . 11
โข (( 1 โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) โ ((๐ ยท 1 ) = 1 โง ( 1 ยท ๐) = 1 )) |
47 | 46 | simprd 497 |
. . . . . . . . . 10
โข (( 1 โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) โ ( 1 ยท ๐) = 1 ) |
48 | 38, 39, 47 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) โ ( 1 ยท ๐) = 1 ) |
49 | 37, 48 | eqtr3d 2775 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) โ ๐ = 1 ) |
50 | 49 | ex 414 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) โ ๐ = 1 )) |
51 | 28, 50 | sylbird 260 |
. . . . . 6
โข (๐ โ ((๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ)) โ ๐ = 1 )) |
52 | 51 | alrimiv 1931 |
. . . . 5
โข (๐ โ โ๐((๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ)) โ ๐ = 1 )) |
53 | | eleq1 2822 |
. . . . . . 7
โข (๐ = 1 โ (๐ โ (Baseโ๐
) โ 1 โ (Baseโ๐
))) |
54 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ = 1 โ (๐(.rโ๐
)๐ฅ) = ( 1 (.rโ๐
)๐ฅ)) |
55 | 54 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ = 1 โ ((๐(.rโ๐
)๐ฅ) = ๐ฅ โ ( 1 (.rโ๐
)๐ฅ) = ๐ฅ)) |
56 | 55 | ovanraleqv 7433 |
. . . . . . 7
โข (๐ = 1 โ (โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ) โ โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ))) |
57 | 53, 56 | anbi12d 632 |
. . . . . 6
โข (๐ = 1 โ ((๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ)) โ ( 1 โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)))) |
58 | 57 | eqeu 3703 |
. . . . 5
โข (( 1 โ
(Baseโ๐
) โง (
1 โ
(Baseโ๐
) โง
โ๐ฅ โ
(Baseโ๐
)(( 1
(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)) โง โ๐((๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ)) โ ๐ = 1 )) โ โ!๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) |
59 | 7, 7, 20, 52, 58 | syl121anc 1376 |
. . . 4
โข (๐ โ โ!๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) |
60 | 57 | iota2 6533 |
. . . 4
โข (( 1 โ ๐ต โง โ!๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) โ (( 1 โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)) โ (โฉ๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) = 1 )) |
61 | 5, 59, 60 | syl2anc 585 |
. . 3
โข (๐ โ (( 1 โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)(( 1 (.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
) 1 ) = ๐ฅ)) โ (โฉ๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) = 1 )) |
62 | 7, 20, 61 | mpbi2and 711 |
. 2
โข (๐ โ (โฉ๐(๐ โ (Baseโ๐
) โง โ๐ฅ โ (Baseโ๐
)((๐(.rโ๐
)๐ฅ) = ๐ฅ โง (๐ฅ(.rโ๐
)๐) = ๐ฅ))) = 1 ) |
63 | 4, 62 | eqtr2id 2786 |
1
โข (๐ โ 1 =
(1rโ๐
)) |