Step | Hyp | Ref
| Expression |
1 | | remulinvcom.2 |
. . 3
โข (๐ โ ๐ต โ โ) |
2 | | remulinvcom.3 |
. . . . 5
โข (๐ โ (๐ด ยท ๐ต) = 1) |
3 | | ax-1ne0 11178 |
. . . . . 6
โข 1 โ
0 |
4 | 3 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ 0) |
5 | 2, 4 | eqnetrd 3008 |
. . . 4
โข (๐ โ (๐ด ยท ๐ต) โ 0) |
6 | | simpr 485 |
. . . . . 6
โข ((๐ โง ๐ต = 0) โ ๐ต = 0) |
7 | 6 | oveq2d 7424 |
. . . . 5
โข ((๐ โง ๐ต = 0) โ (๐ด ยท ๐ต) = (๐ด ยท 0)) |
8 | | remulinvcom.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
9 | 8 | adantr 481 |
. . . . . 6
โข ((๐ โง ๐ต = 0) โ ๐ด โ โ) |
10 | | remul01 41281 |
. . . . . 6
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
11 | 9, 10 | syl 17 |
. . . . 5
โข ((๐ โง ๐ต = 0) โ (๐ด ยท 0) = 0) |
12 | 7, 11 | eqtrd 2772 |
. . . 4
โข ((๐ โง ๐ต = 0) โ (๐ด ยท ๐ต) = 0) |
13 | 5, 12 | mteqand 3033 |
. . 3
โข (๐ โ ๐ต โ 0) |
14 | | ax-rrecex 11181 |
. . 3
โข ((๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = 1) |
15 | 1, 13, 14 | syl2anc 584 |
. 2
โข (๐ โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = 1) |
16 | | simprl 769 |
. . . 4
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ ๐ฅ โ โ) |
17 | | simprr 771 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ (๐ต ยท ๐ฅ) = 1) |
18 | 3 | a1i 11 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ 1 โ 0) |
19 | 17, 18 | eqnetrd 3008 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ (๐ต ยท ๐ฅ) โ 0) |
20 | | simpr 485 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง ๐ฅ = 0) โ ๐ฅ = 0) |
21 | 20 | oveq2d 7424 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง ๐ฅ = 0) โ (๐ต ยท ๐ฅ) = (๐ต ยท 0)) |
22 | 1 | ad2antrr 724 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง ๐ฅ = 0) โ ๐ต โ โ) |
23 | | remul01 41281 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต ยท 0) =
0) |
24 | 22, 23 | syl 17 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง ๐ฅ = 0) โ (๐ต ยท 0) = 0) |
25 | 21, 24 | eqtrd 2772 |
. . . . 5
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง ๐ฅ = 0) โ (๐ต ยท ๐ฅ) = 0) |
26 | 19, 25 | mteqand 3033 |
. . . 4
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ ๐ฅ โ 0) |
27 | | ax-rrecex 11181 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฅ โ 0) โ โ๐ฆ โ โ (๐ฅ ยท ๐ฆ) = 1) |
28 | 16, 26, 27 | syl2anc 584 |
. . 3
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ โ๐ฆ โ โ (๐ฅ ยท ๐ฆ) = 1) |
29 | | simplrr 776 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ต ยท ๐ฅ) = 1) |
30 | 29 | oveq2d 7424 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท (๐ต ยท ๐ฅ)) = (๐ด ยท 1)) |
31 | 30 | oveq1d 7423 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท (๐ต ยท ๐ฅ)) ยท ๐ฆ) = ((๐ด ยท 1) ยท ๐ฆ)) |
32 | 8 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
33 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
34 | 32, 33 | remulcld 11243 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท ๐ต) โ โ) |
35 | 34 | recnd 11241 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท ๐ต) โ โ) |
36 | | simplrl 775 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ฅ โ โ) |
37 | 36 | recnd 11241 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ฅ โ โ) |
38 | | simprl 769 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
39 | 38 | recnd 11241 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
40 | 35, 37, 39 | mulassd 11236 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (((๐ด ยท ๐ต) ยท ๐ฅ) ยท ๐ฆ) = ((๐ด ยท ๐ต) ยท (๐ฅ ยท ๐ฆ))) |
41 | 32 | recnd 11241 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
42 | 33 | recnd 11241 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
43 | 41, 42, 37 | mulassd 11236 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท ๐ต) ยท ๐ฅ) = (๐ด ยท (๐ต ยท ๐ฅ))) |
44 | 43 | oveq1d 7423 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (((๐ด ยท ๐ต) ยท ๐ฅ) ยท ๐ฆ) = ((๐ด ยท (๐ต ยท ๐ฅ)) ยท ๐ฆ)) |
45 | 2 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท ๐ต) = 1) |
46 | | simprr 771 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ฅ ยท ๐ฆ) = 1) |
47 | 45, 46 | oveq12d 7426 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท ๐ต) ยท (๐ฅ ยท ๐ฆ)) = (1 ยท 1)) |
48 | | 1t1e1ALT 41178 |
. . . . . . . . 9
โข (1
ยท 1) = 1 |
49 | 47, 48 | eqtrdi 2788 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท ๐ต) ยท (๐ฅ ยท ๐ฆ)) = 1) |
50 | 40, 44, 49 | 3eqtr3d 2780 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท (๐ต ยท ๐ฅ)) ยท ๐ฆ) = 1) |
51 | | ax-1rid 11179 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
52 | 32, 51 | syl 17 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท 1) = ๐ด) |
53 | 52 | oveq1d 7423 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท 1) ยท ๐ฆ) = (๐ด ยท ๐ฆ)) |
54 | 31, 50, 53 | 3eqtr3rd 2781 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท ๐ฆ) = 1) |
55 | 54, 46 | eqtr4d 2775 |
. . . . 5
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ด ยท ๐ฆ) = (๐ฅ ยท ๐ฆ)) |
56 | 3 | a1i 11 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ 1 โ 0) |
57 | 46, 56 | eqnetrd 3008 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ฅ ยท ๐ฆ) โ 0) |
58 | | simpr 485 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ฆ = 0) โ ๐ฆ = 0) |
59 | 58 | oveq2d 7424 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ฆ = 0) โ (๐ฅ ยท ๐ฆ) = (๐ฅ ยท 0)) |
60 | 36 | adantr 481 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ฆ = 0) โ ๐ฅ โ โ) |
61 | | remul01 41281 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (๐ฅ ยท 0) =
0) |
62 | 60, 61 | syl 17 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ฆ = 0) โ (๐ฅ ยท 0) = 0) |
63 | 59, 62 | eqtrd 2772 |
. . . . . . 7
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ฆ = 0) โ (๐ฅ ยท ๐ฆ) = 0) |
64 | 57, 63 | mteqand 3033 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ฆ โ 0) |
65 | 32, 36, 38, 64 | remulcan2d 41179 |
. . . . 5
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ((๐ด ยท ๐ฆ) = (๐ฅ ยท ๐ฆ) โ ๐ด = ๐ฅ)) |
66 | 55, 65 | mpbid 231 |
. . . 4
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ ๐ด = ๐ฅ) |
67 | | simpr 485 |
. . . . . 6
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ด = ๐ฅ) โ ๐ด = ๐ฅ) |
68 | 67 | oveq2d 7424 |
. . . . 5
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ด = ๐ฅ) โ (๐ต ยท ๐ด) = (๐ต ยท ๐ฅ)) |
69 | 17 | ad2antrr 724 |
. . . . 5
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ด = ๐ฅ) โ (๐ต ยท ๐ฅ) = 1) |
70 | 68, 69 | eqtrd 2772 |
. . . 4
โข ((((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โง ๐ด = ๐ฅ) โ (๐ต ยท ๐ด) = 1) |
71 | 66, 70 | mpdan 685 |
. . 3
โข (((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โง (๐ฆ โ โ โง (๐ฅ ยท ๐ฆ) = 1)) โ (๐ต ยท ๐ด) = 1) |
72 | 28, 71 | rexlimddv 3161 |
. 2
โข ((๐ โง (๐ฅ โ โ โง (๐ต ยท ๐ฅ) = 1)) โ (๐ต ยท ๐ด) = 1) |
73 | 15, 72 | rexlimddv 3161 |
1
โข (๐ โ (๐ต ยท ๐ด) = 1) |