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