Step | Hyp | Ref
| Expression |
1 | | r19.26-2 3130 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
2 | | eqtr2 2748 |
. . . . . . 7
โข (((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
3 | 2 | 2ralimi 3115 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
4 | 1, 3 | sylbir 234 |
. . . . 5
โข
((โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
5 | | hoeq1 31577 |
. . . . . 6
โข ((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ขโ๐ฅ)
ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ) โ ๐ข = ๐ฃ)) |
6 | 5 | biimpa 476 |
. . . . 5
โข (((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ขโ๐ฅ)
ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ ๐ข = ๐ฃ) |
7 | 4, 6 | sylan2 592 |
. . . 4
โข (((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โง (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
8 | 7 | an4s 657 |
. . 3
โข (((๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
9 | 8 | gen2 1790 |
. 2
โข
โ๐ขโ๐ฃ(((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
10 | | feq1 6689 |
. . . 4
โข (๐ข = ๐ฃ โ (๐ข: โโถ โ โ ๐ฃ: โโถ
โ)) |
11 | | fveq1 6881 |
. . . . . . 7
โข (๐ข = ๐ฃ โ (๐ขโ๐ฅ) = (๐ฃโ๐ฅ)) |
12 | 11 | oveq1d 7417 |
. . . . . 6
โข (๐ข = ๐ฃ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
13 | 12 | eqeq2d 2735 |
. . . . 5
โข (๐ข = ๐ฃ โ ((๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
14 | 13 | 2ralbidv 3210 |
. . . 4
โข (๐ข = ๐ฃ โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
15 | 10, 14 | anbi12d 630 |
. . 3
โข (๐ข = ๐ฃ โ ((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)))) |
16 | 15 | mo4 2552 |
. 2
โข
(โ*๐ข(๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ โ๐ขโ๐ฃ(((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ)) |
17 | 9, 16 | mpbir 230 |
1
โข
โ*๐ข(๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) |