Step | Hyp | Ref
| Expression |
1 | | dvhvaddval.a |
. 2
âĒ + = (ð â (ð Ã ðļ), ð â (ð Ã ðļ) âĶ âĻ((1st
âð) â
(1st âð)),
((2nd âð)
âĻĢ
(2nd âð))âĐ) |
2 | | fveq2 6843 |
. . . . 5
âĒ (ð = â â (1st âð) = (1st ââ)) |
3 | 2 | coeq1d 5818 |
. . . 4
âĒ (ð = â â ((1st âð) â (1st
âð)) =
((1st ââ)
â (1st âð))) |
4 | | fveq2 6843 |
. . . . 5
âĒ (ð = â â (2nd âð) = (2nd ââ)) |
5 | 4 | oveq1d 7373 |
. . . 4
âĒ (ð = â â ((2nd âð) âĻĢ (2nd
âð)) =
((2nd ââ)
âĻĢ
(2nd âð))) |
6 | 3, 5 | opeq12d 4839 |
. . 3
âĒ (ð = â â âĻ((1st âð) â (1st
âð)),
((2nd âð)
âĻĢ
(2nd âð))âĐ = âĻ((1st
ââ) â
(1st âð)),
((2nd ââ)
âĻĢ
(2nd âð))âĐ) |
7 | | fveq2 6843 |
. . . . 5
âĒ (ð = ð â (1st âð) = (1st âð)) |
8 | 7 | coeq2d 5819 |
. . . 4
âĒ (ð = ð â ((1st ââ) â (1st
âð)) =
((1st ââ)
â (1st âð))) |
9 | | fveq2 6843 |
. . . . 5
âĒ (ð = ð â (2nd âð) = (2nd âð)) |
10 | 9 | oveq2d 7374 |
. . . 4
âĒ (ð = ð â ((2nd ââ) âĻĢ (2nd
âð)) =
((2nd ââ)
âĻĢ
(2nd âð))) |
11 | 8, 10 | opeq12d 4839 |
. . 3
âĒ (ð = ð â âĻ((1st ââ) â (1st
âð)),
((2nd ââ)
âĻĢ
(2nd âð))âĐ = âĻ((1st
ââ) â
(1st âð)),
((2nd ââ)
âĻĢ
(2nd âð))âĐ) |
12 | 6, 11 | cbvmpov 7453 |
. 2
âĒ (ð â (ð Ã ðļ), ð â (ð Ã ðļ) âĶ âĻ((1st
âð) â
(1st âð)),
((2nd âð)
âĻĢ
(2nd âð))âĐ) = (â â (ð à ðļ), ð â (ð à ðļ) âĶ âĻ((1st
ââ) â
(1st âð)),
((2nd ââ)
âĻĢ
(2nd âð))âĐ) |
13 | 1, 12 | eqtri 2765 |
1
âĒ + = (â â (ð Ã ðļ), ð â (ð Ã ðļ) âĶ âĻ((1st
ââ) â
(1st âð)),
((2nd ââ)
âĻĢ
(2nd âð))âĐ) |