Step |
Hyp |
Ref |
Expression |
1 |
|
recex |
โข ( ( ๐ต โ โ โง ๐ต โ 0 ) โ โ ๐ฆ โ โ ( ๐ต ยท ๐ฆ ) = 1 ) |
2 |
1
|
3adant1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ โ ๐ฆ โ โ ( ๐ต ยท ๐ฆ ) = 1 ) |
3 |
|
simprl |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ๐ฆ โ โ ) |
4 |
|
simpll |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ๐ด โ โ ) |
5 |
3 4
|
mulcld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ( ๐ฆ ยท ๐ด ) โ โ ) |
6 |
|
oveq1 |
โข ( ( ๐ต ยท ๐ฆ ) = 1 โ ( ( ๐ต ยท ๐ฆ ) ยท ๐ด ) = ( 1 ยท ๐ด ) ) |
7 |
6
|
ad2antll |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ( ( ๐ต ยท ๐ฆ ) ยท ๐ด ) = ( 1 ยท ๐ด ) ) |
8 |
|
simplr |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ๐ต โ โ ) |
9 |
8 3 4
|
mulassd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ( ( ๐ต ยท ๐ฆ ) ยท ๐ด ) = ( ๐ต ยท ( ๐ฆ ยท ๐ด ) ) ) |
10 |
4
|
mulid2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ( 1 ยท ๐ด ) = ๐ด ) |
11 |
7 9 10
|
3eqtr3d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ ( ๐ต ยท ( ๐ฆ ยท ๐ด ) ) = ๐ด ) |
12 |
|
oveq2 |
โข ( ๐ฅ = ( ๐ฆ ยท ๐ด ) โ ( ๐ต ยท ๐ฅ ) = ( ๐ต ยท ( ๐ฆ ยท ๐ด ) ) ) |
13 |
12
|
eqeq1d |
โข ( ๐ฅ = ( ๐ฆ ยท ๐ด ) โ ( ( ๐ต ยท ๐ฅ ) = ๐ด โ ( ๐ต ยท ( ๐ฆ ยท ๐ด ) ) = ๐ด ) ) |
14 |
13
|
rspcev |
โข ( ( ( ๐ฆ ยท ๐ด ) โ โ โง ( ๐ต ยท ( ๐ฆ ยท ๐ด ) ) = ๐ด ) โ โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) |
15 |
5 11 14
|
syl2anc |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ฆ โ โ โง ( ๐ต ยท ๐ฆ ) = 1 ) ) โ โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) |
16 |
15
|
rexlimdvaa |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( โ ๐ฆ โ โ ( ๐ต ยท ๐ฆ ) = 1 โ โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) ) |
17 |
16
|
3adant3 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ ( โ ๐ฆ โ โ ( ๐ต ยท ๐ฆ ) = 1 โ โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) ) |
18 |
2 17
|
mpd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) |
19 |
|
eqtr3 |
โข ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ( ๐ต ยท ๐ฅ ) = ( ๐ต ยท ๐ฆ ) ) |
20 |
|
mulcan |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ โง ( ๐ต โ โ โง ๐ต โ 0 ) ) โ ( ( ๐ต ยท ๐ฅ ) = ( ๐ต ยท ๐ฆ ) โ ๐ฅ = ๐ฆ ) ) |
21 |
19 20
|
syl5ib |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ โง ( ๐ต โ โ โง ๐ต โ 0 ) ) โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) |
22 |
21
|
3expa |
โข ( ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โง ( ๐ต โ โ โง ๐ต โ 0 ) ) โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) |
23 |
22
|
expcom |
โข ( ( ๐ต โ โ โง ๐ต โ 0 ) โ ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) ) |
24 |
23
|
3adant1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) ) |
25 |
24
|
ralrimivv |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ โ ๐ฅ โ โ โ ๐ฆ โ โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) |
26 |
|
oveq2 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ต ยท ๐ฅ ) = ( ๐ต ยท ๐ฆ ) ) |
27 |
26
|
eqeq1d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ต ยท ๐ฅ ) = ๐ด โ ( ๐ต ยท ๐ฆ ) = ๐ด ) ) |
28 |
27
|
reu4 |
โข ( โ! ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด โ ( โ ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด โง โ ๐ฅ โ โ โ ๐ฆ โ โ ( ( ( ๐ต ยท ๐ฅ ) = ๐ด โง ( ๐ต ยท ๐ฆ ) = ๐ด ) โ ๐ฅ = ๐ฆ ) ) ) |
29 |
18 25 28
|
sylanbrc |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0 ) โ โ! ๐ฅ โ โ ( ๐ต ยท ๐ฅ ) = ๐ด ) |