Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
โข (๐ง = ๐บ โ ๐ง = ๐บ) |
2 | 1, 1 | coeq12d 5821 |
. . . . 5
โข (๐ง = ๐บ โ (๐ง โ ๐ง) = (๐บ โ ๐บ)) |
3 | 2 | oveq2d 7374 |
. . . 4
โข (๐ง = ๐บ โ (๐ โop (๐ง โ ๐ง)) = (๐ โop (๐บ โ ๐บ))) |
4 | 3 | oveq2d 7374 |
. . 3
โข (๐ง = ๐บ โ ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง))) = ((1 / 2) ยทop
(๐ โop
(๐บ โ ๐บ)))) |
5 | 1, 4 | oveq12d 7376 |
. 2
โข (๐ง = ๐บ โ (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง)))) = (๐บ +op ((1 / 2)
ยทop (๐ โop (๐บ โ ๐บ))))) |
6 | | eqidd 2734 |
. 2
โข (๐ค = ๐ป โ (๐บ +op ((1 / 2)
ยทop (๐ โop (๐บ โ ๐บ)))) = (๐บ +op ((1 / 2)
ยทop (๐ โop (๐บ โ ๐บ))))) |
7 | | opsqrlem2.2 |
. . 3
โข ๐ = (๐ฅ โ HrmOp, ๐ฆ โ HrmOp โฆ (๐ฅ +op ((1 / 2)
ยทop (๐ โop (๐ฅ โ ๐ฅ))))) |
8 | | id 22 |
. . . . 5
โข (๐ฅ = ๐ง โ ๐ฅ = ๐ง) |
9 | 8, 8 | coeq12d 5821 |
. . . . . . 7
โข (๐ฅ = ๐ง โ (๐ฅ โ ๐ฅ) = (๐ง โ ๐ง)) |
10 | 9 | oveq2d 7374 |
. . . . . 6
โข (๐ฅ = ๐ง โ (๐ โop (๐ฅ โ ๐ฅ)) = (๐ โop (๐ง โ ๐ง))) |
11 | 10 | oveq2d 7374 |
. . . . 5
โข (๐ฅ = ๐ง โ ((1 / 2) ยทop
(๐ โop
(๐ฅ โ ๐ฅ))) = ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง)))) |
12 | 8, 11 | oveq12d 7376 |
. . . 4
โข (๐ฅ = ๐ง โ (๐ฅ +op ((1 / 2)
ยทop (๐ โop (๐ฅ โ ๐ฅ)))) = (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง))))) |
13 | | eqidd 2734 |
. . . 4
โข (๐ฆ = ๐ค โ (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง)))) = (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง))))) |
14 | 12, 13 | cbvmpov 7453 |
. . 3
โข (๐ฅ โ HrmOp, ๐ฆ โ HrmOp โฆ (๐ฅ +op ((1 / 2)
ยทop (๐ โop (๐ฅ โ ๐ฅ))))) = (๐ง โ HrmOp, ๐ค โ HrmOp โฆ (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง))))) |
15 | 7, 14 | eqtri 2761 |
. 2
โข ๐ = (๐ง โ HrmOp, ๐ค โ HrmOp โฆ (๐ง +op ((1 / 2)
ยทop (๐ โop (๐ง โ ๐ง))))) |
16 | | ovex 7391 |
. 2
โข (๐บ +op ((1 / 2)
ยทop (๐ โop (๐บ โ ๐บ)))) โ V |
17 | 5, 6, 15, 16 | ovmpo 7516 |
1
โข ((๐บ โ HrmOp โง ๐ป โ HrmOp) โ (๐บ๐๐ป) = (๐บ +op ((1 / 2)
ยทop (๐ โop (๐บ โ ๐บ))))) |