Step | Hyp | Ref
| Expression |
1 | | opex 5426 |
. 2
โข
โจ((๐ด
ยทR ๐ถ) +R
(-1R ยทR (๐ต
ยทR ๐ท))), ((๐ต ยทR ๐ถ) +R
(๐ด
ยทR ๐ท))โฉ โ V |
2 | | oveq1 7369 |
. . . . 5
โข (๐ค = ๐ด โ (๐ค ยทR ๐ข) = (๐ด ยทR ๐ข)) |
3 | | oveq1 7369 |
. . . . . 6
โข (๐ฃ = ๐ต โ (๐ฃ ยทR ๐) = (๐ต ยทR ๐)) |
4 | 3 | oveq2d 7378 |
. . . . 5
โข (๐ฃ = ๐ต โ (-1R
ยทR (๐ฃ ยทR ๐)) =
(-1R ยทR (๐ต
ยทR ๐))) |
5 | 2, 4 | oveqan12d 7381 |
. . . 4
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))) = ((๐ด ยทR ๐ข) +R
(-1R ยทR (๐ต
ยทR ๐)))) |
6 | | oveq1 7369 |
. . . . 5
โข (๐ฃ = ๐ต โ (๐ฃ ยทR ๐ข) = (๐ต ยทR ๐ข)) |
7 | | oveq1 7369 |
. . . . 5
โข (๐ค = ๐ด โ (๐ค ยทR ๐) = (๐ด ยทR ๐)) |
8 | 6, 7 | oveqan12rd 7382 |
. . . 4
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐)) = ((๐ต ยทR ๐ข) +R
(๐ด
ยทR ๐))) |
9 | 5, 8 | opeq12d 4843 |
. . 3
โข ((๐ค = ๐ด โง ๐ฃ = ๐ต) โ โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ = โจ((๐ด ยทR ๐ข) +R
(-1R ยทR (๐ต
ยทR ๐))), ((๐ต ยทR ๐ข) +R
(๐ด
ยทR ๐))โฉ) |
10 | | oveq2 7370 |
. . . . 5
โข (๐ข = ๐ถ โ (๐ด ยทR ๐ข) = (๐ด ยทR ๐ถ)) |
11 | | oveq2 7370 |
. . . . . 6
โข (๐ = ๐ท โ (๐ต ยทR ๐) = (๐ต ยทR ๐ท)) |
12 | 11 | oveq2d 7378 |
. . . . 5
โข (๐ = ๐ท โ (-1R
ยทR (๐ต ยทR ๐)) =
(-1R ยทR (๐ต
ยทR ๐ท))) |
13 | 10, 12 | oveqan12d 7381 |
. . . 4
โข ((๐ข = ๐ถ โง ๐ = ๐ท) โ ((๐ด ยทR ๐ข) +R
(-1R ยทR (๐ต
ยทR ๐))) = ((๐ด ยทR ๐ถ) +R
(-1R ยทR (๐ต
ยทR ๐ท)))) |
14 | | oveq2 7370 |
. . . . 5
โข (๐ข = ๐ถ โ (๐ต ยทR ๐ข) = (๐ต ยทR ๐ถ)) |
15 | | oveq2 7370 |
. . . . 5
โข (๐ = ๐ท โ (๐ด ยทR ๐) = (๐ด ยทR ๐ท)) |
16 | 14, 15 | oveqan12d 7381 |
. . . 4
โข ((๐ข = ๐ถ โง ๐ = ๐ท) โ ((๐ต ยทR ๐ข) +R
(๐ด
ยทR ๐)) = ((๐ต ยทR ๐ถ) +R
(๐ด
ยทR ๐ท))) |
17 | 13, 16 | opeq12d 4843 |
. . 3
โข ((๐ข = ๐ถ โง ๐ = ๐ท) โ โจ((๐ด ยทR ๐ข) +R
(-1R ยทR (๐ต
ยทR ๐))), ((๐ต ยทR ๐ข) +R
(๐ด
ยทR ๐))โฉ = โจ((๐ด ยทR ๐ถ) +R
(-1R ยทR (๐ต
ยทR ๐ท))), ((๐ต ยทR ๐ถ) +R
(๐ด
ยทR ๐ท))โฉ) |
18 | 9, 17 | sylan9eq 2797 |
. 2
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ = โจ((๐ด ยทR ๐ถ) +R
(-1R ยทR (๐ต
ยทR ๐ท))), ((๐ต ยทR ๐ถ) +R
(๐ด
ยทR ๐ท))โฉ) |
19 | | df-mul 11070 |
. . 3
โข ยท
= {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ))} |
20 | | df-c 11064 |
. . . . . . 7
โข โ =
(R ร R) |
21 | 20 | eleq2i 2830 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ (R ร
R)) |
22 | 20 | eleq2i 2830 |
. . . . . 6
โข (๐ฆ โ โ โ ๐ฆ โ (R ร
R)) |
23 | 21, 22 | anbi12i 628 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ โ (R ร
R) โง ๐ฆ
โ (R ร R))) |
24 | 23 | anbi1i 625 |
. . . 4
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ)) โ ((๐ฅ โ (R ร
R) โง ๐ฆ
โ (R ร R)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ))) |
25 | 24 | oprabbii 7429 |
. . 3
โข
{โจโจ๐ฅ,
๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ))} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (R ร
R) โง ๐ฆ
โ (R ร R)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ))} |
26 | 19, 25 | eqtri 2765 |
. 2
โข ยท
= {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (R ร
R) โง ๐ฆ
โ (R ร R)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทR ๐ข) +R
(-1R ยทR (๐ฃ
ยทR ๐))), ((๐ฃ ยทR ๐ข) +R
(๐ค
ยทR ๐))โฉ))} |
27 | 1, 18, 26 | ov3 7522 |
1
โข (((๐ด โ R โง
๐ต โ R)
โง (๐ถ โ
R โง ๐ท
โ R)) โ (โจ๐ด, ๐ตโฉ ยท โจ๐ถ, ๐ทโฉ) = โจ((๐ด ยทR ๐ถ) +R
(-1R ยทR (๐ต
ยทR ๐ท))), ((๐ต ยทR ๐ถ) +R
(๐ด
ยทR ๐ท))โฉ) |