Step | Hyp | Ref
| Expression |
1 | | r19.26-2 3132 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
2 | | eqtr2 2757 |
. . . . . . 7
โข (((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
3 | 2 | 2ralimi 3123 |
. . . . . 6
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
4 | 1, 3 | sylbir 234 |
. . . . 5
โข
((โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
5 | | hoeq1 30814 |
. . . . . 6
โข ((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ขโ๐ฅ)
ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ) โ ๐ข = ๐ฃ)) |
6 | 5 | biimpa 478 |
. . . . 5
โข (((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐ขโ๐ฅ)
ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) โ ๐ข = ๐ฃ) |
7 | 4, 6 | sylan2 594 |
. . . 4
โข (((๐ข: โโถ โ โง
๐ฃ: โโถ โ)
โง (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
8 | 7 | an4s 659 |
. . 3
โข (((๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
9 | 8 | gen2 1799 |
. 2
โข
โ๐ขโ๐ฃ(((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ) |
10 | | feq1 6650 |
. . . 4
โข (๐ข = ๐ฃ โ (๐ข: โโถ โ โ ๐ฃ: โโถ
โ)) |
11 | | fveq1 6842 |
. . . . . . 7
โข (๐ข = ๐ฃ โ (๐ขโ๐ฅ) = (๐ฃโ๐ฅ)) |
12 | 11 | oveq1d 7373 |
. . . . . 6
โข (๐ข = ๐ฃ โ ((๐ขโ๐ฅ) ยทih ๐ฆ) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)) |
13 | 12 | eqeq2d 2744 |
. . . . 5
โข (๐ข = ๐ฃ โ ((๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
14 | 13 | 2ralbidv 3209 |
. . . 4
โข (๐ข = ๐ฃ โ (โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) |
15 | 10, 14 | anbi12d 632 |
. . 3
โข (๐ข = ๐ฃ โ ((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ)))) |
16 | 15 | mo4 2561 |
. 2
โข
(โ*๐ข(๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โ โ๐ขโ๐ฃ(((๐ข: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) โง (๐ฃ: โโถ โ โง โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ฃโ๐ฅ) ยทih ๐ฆ))) โ ๐ข = ๐ฃ)) |
17 | 9, 16 | mpbir 230 |
1
โข
โ*๐ข(๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐ขโ๐ฅ) ยทih ๐ฆ)) |