Step |
Hyp |
Ref |
Expression |
1 |
|
sqgt0sr |
โข ( ( ๐ด โ R โง ๐ด โ 0R ) โ 0R <R ( ๐ด ยทR ๐ด ) ) |
2 |
|
mulclsr |
โข ( ( ๐ด โ R โง ๐ฆ โ R ) โ ( ๐ด ยทR ๐ฆ ) โ R ) |
3 |
|
mulasssr |
โข ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = ( ๐ด ยทR ( ๐ด ยทR ๐ฆ ) ) |
4 |
3
|
eqeq1i |
โข ( ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = 1R โ ( ๐ด ยทR ( ๐ด ยทR ๐ฆ ) ) = 1R ) |
5 |
|
oveq2 |
โข ( ๐ฅ = ( ๐ด ยทR ๐ฆ ) โ ( ๐ด ยทR ๐ฅ ) = ( ๐ด ยทR ( ๐ด ยทR ๐ฆ ) ) ) |
6 |
5
|
eqeq1d |
โข ( ๐ฅ = ( ๐ด ยทR ๐ฆ ) โ ( ( ๐ด ยทR ๐ฅ ) = 1R โ ( ๐ด ยทR ( ๐ด ยทR ๐ฆ ) ) = 1R ) ) |
7 |
6
|
rspcev |
โข ( ( ( ๐ด ยทR ๐ฆ ) โ R โง ( ๐ด ยทR ( ๐ด ยทR ๐ฆ ) ) = 1R ) โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) |
8 |
4 7
|
sylan2b |
โข ( ( ( ๐ด ยทR ๐ฆ ) โ R โง ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = 1R ) โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) |
9 |
2 8
|
sylan |
โข ( ( ( ๐ด โ R โง ๐ฆ โ R ) โง ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = 1R ) โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) |
10 |
9
|
rexlimdva2 |
โข ( ๐ด โ R โ ( โ ๐ฆ โ R ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = 1R โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) ) |
11 |
|
recexsrlem |
โข ( 0R <R ( ๐ด ยทR ๐ด ) โ โ ๐ฆ โ R ( ( ๐ด ยทR ๐ด ) ยทR ๐ฆ ) = 1R ) |
12 |
10 11
|
impel |
โข ( ( ๐ด โ R โง 0R <R ( ๐ด ยทR ๐ด ) ) โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) |
13 |
1 12
|
syldan |
โข ( ( ๐ด โ R โง ๐ด โ 0R ) โ โ ๐ฅ โ R ( ๐ด ยทR ๐ฅ ) = 1R ) |