Step | Hyp | Ref
| Expression |
1 | | elreal 11128 |
. . . 4
โข (๐ด โ โ โ
โ๐ฆ โ
R โจ๐ฆ,
0Rโฉ = ๐ด) |
2 | | df-rex 3069 |
. . . 4
โข
(โ๐ฆ โ
R โจ๐ฆ,
0Rโฉ = ๐ด โ โ๐ฆ(๐ฆ โ R โง โจ๐ฆ,
0Rโฉ = ๐ด)) |
3 | 1, 2 | bitri 274 |
. . 3
โข (๐ด โ โ โ
โ๐ฆ(๐ฆ โ R โง โจ๐ฆ,
0Rโฉ = ๐ด)) |
4 | | neeq1 3001 |
. . . 4
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (โจ๐ฆ, 0Rโฉ โ 0
โ ๐ด โ
0)) |
5 | | oveq1 7418 |
. . . . . 6
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = (๐ด ยท ๐ฅ)) |
6 | 5 | eqeq1d 2732 |
. . . . 5
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ ((โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1 โ (๐ด ยท ๐ฅ) = 1)) |
7 | 6 | rexbidv 3176 |
. . . 4
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (โ๐ฅ โ โ (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
8 | 4, 7 | imbi12d 343 |
. . 3
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ ((โจ๐ฆ, 0Rโฉ โ 0
โ โ๐ฅ โ
โ (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1) โ (๐ด โ 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1))) |
9 | | df-0 11119 |
. . . . . . 7
โข 0 =
โจ0R,
0Rโฉ |
10 | 9 | eqeq2i 2743 |
. . . . . 6
โข
(โจ๐ฆ,
0Rโฉ = 0 โ โจ๐ฆ, 0Rโฉ =
โจ0R,
0Rโฉ) |
11 | | vex 3476 |
. . . . . . 7
โข ๐ฆ โ V |
12 | 11 | eqresr 11134 |
. . . . . 6
โข
(โจ๐ฆ,
0Rโฉ = โจ0R,
0Rโฉ โ ๐ฆ =
0R) |
13 | 10, 12 | bitri 274 |
. . . . 5
โข
(โจ๐ฆ,
0Rโฉ = 0 โ ๐ฆ =
0R) |
14 | 13 | necon3bii 2991 |
. . . 4
โข
(โจ๐ฆ,
0Rโฉ โ 0 โ ๐ฆ โ
0R) |
15 | | recexsr 11104 |
. . . . . 6
โข ((๐ฆ โ R โง
๐ฆ โ
0R) โ โ๐ง โ R (๐ฆ ยทR ๐ง) =
1R) |
16 | 15 | ex 411 |
. . . . 5
โข (๐ฆ โ R โ
(๐ฆ โ
0R โ โ๐ง โ R (๐ฆ ยทR ๐ง) =
1R)) |
17 | | opelreal 11127 |
. . . . . . . . . 10
โข
(โจ๐ง,
0Rโฉ โ โ โ ๐ง โ R) |
18 | 17 | anbi1i 622 |
. . . . . . . . 9
โข
((โจ๐ง,
0Rโฉ โ โ โง (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1)
โ (๐ง โ
R โง (โจ๐ฆ, 0Rโฉ ยท
โจ๐ง,
0Rโฉ) = 1)) |
19 | | mulresr 11136 |
. . . . . . . . . . . 12
โข ((๐ฆ โ R โง
๐ง โ R)
โ (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) =
โจ(๐ฆ
ยทR ๐ง),
0Rโฉ) |
20 | 19 | eqeq1d 2732 |
. . . . . . . . . . 11
โข ((๐ฆ โ R โง
๐ง โ R)
โ ((โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1
โ โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
1)) |
21 | | df-1 11120 |
. . . . . . . . . . . . 13
โข 1 =
โจ1R,
0Rโฉ |
22 | 21 | eqeq2i 2743 |
. . . . . . . . . . . 12
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ = 1
โ โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R,
0Rโฉ) |
23 | | ovex 7444 |
. . . . . . . . . . . . 13
โข (๐ฆ
ยทR ๐ง) โ V |
24 | 23 | eqresr 11134 |
. . . . . . . . . . . 12
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R, 0Rโฉ โ
(๐ฆ
ยทR ๐ง) =
1R) |
25 | 22, 24 | bitri 274 |
. . . . . . . . . . 11
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ = 1
โ (๐ฆ
ยทR ๐ง) =
1R) |
26 | 20, 25 | bitrdi 286 |
. . . . . . . . . 10
โข ((๐ฆ โ R โง
๐ง โ R)
โ ((โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1
โ (๐ฆ
ยทR ๐ง) =
1R)) |
27 | 26 | pm5.32da 577 |
. . . . . . . . 9
โข (๐ฆ โ R โ
((๐ง โ R
โง (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1)
โ (๐ง โ
R โง (๐ฆ
ยทR ๐ง) =
1R))) |
28 | 18, 27 | bitrid 282 |
. . . . . . . 8
โข (๐ฆ โ R โ
((โจ๐ง,
0Rโฉ โ โ โง (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1)
โ (๐ง โ
R โง (๐ฆ
ยทR ๐ง) =
1R))) |
29 | | oveq2 7419 |
. . . . . . . . . 10
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
(โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = (โจ๐ฆ, 0Rโฉ ยท
โจ๐ง,
0Rโฉ)) |
30 | 29 | eqeq1d 2732 |
. . . . . . . . 9
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
((โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1 โ (โจ๐ฆ, 0Rโฉ ยท
โจ๐ง,
0Rโฉ) = 1)) |
31 | 30 | rspcev 3611 |
. . . . . . . 8
โข
((โจ๐ง,
0Rโฉ โ โ โง (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1)
โ โ๐ฅ โ
โ (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1) |
32 | 28, 31 | syl6bir 253 |
. . . . . . 7
โข (๐ฆ โ R โ
((๐ง โ R
โง (๐ฆ
ยทR ๐ง) = 1R) โ
โ๐ฅ โ โ
(โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1)) |
33 | 32 | expd 414 |
. . . . . 6
โข (๐ฆ โ R โ
(๐ง โ R
โ ((๐ฆ
ยทR ๐ง) = 1R โ
โ๐ฅ โ โ
(โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1))) |
34 | 33 | rexlimdv 3151 |
. . . . 5
โข (๐ฆ โ R โ
(โ๐ง โ
R (๐ฆ
ยทR ๐ง) = 1R โ
โ๐ฅ โ โ
(โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1)) |
35 | 16, 34 | syld 47 |
. . . 4
โข (๐ฆ โ R โ
(๐ฆ โ
0R โ โ๐ฅ โ โ (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1)) |
36 | 14, 35 | biimtrid 241 |
. . 3
โข (๐ฆ โ R โ
(โจ๐ฆ,
0Rโฉ โ 0 โ โ๐ฅ โ โ (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1)) |
37 | 3, 8, 36 | gencl 3514 |
. 2
โข (๐ด โ โ โ (๐ด โ 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
38 | 37 | imp 405 |
1
โข ((๐ด โ โ โง ๐ด โ 0) โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1) |