Step | Hyp | Ref
| Expression |
1 | | ralcom 3271 |
. . . 4
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฆ โ โ โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
2 | | fveq2 6843 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ (๐โ๐ง) = (๐โ๐ฆ)) |
3 | 2 | oveq2d 7374 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (๐ฅ ยทih (๐โ๐ง)) = (๐ฅ ยทih (๐โ๐ฆ))) |
4 | | oveq2 7366 |
. . . . . . 7
โข (๐ง = ๐ฆ โ ((๐โ๐ฅ) ยทih ๐ง) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
5 | 3, 4 | eqeq12d 2749 |
. . . . . 6
โข (๐ง = ๐ฆ โ ((๐ฅ ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
6 | 5 | ralbidv 3171 |
. . . . 5
โข (๐ง = ๐ฆ โ (โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
7 | 6 | cbvralvw 3224 |
. . . 4
โข
(โ๐ง โ
โ โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ โ๐ฆ โ โ โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
8 | 1, 7 | bitr4i 278 |
. . 3
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ง โ โ โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง)) |
9 | | oveq1 7365 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ฅ ยทih (๐โ๐ง)) = (๐ฆ ยทih (๐โ๐ง))) |
10 | | fveq2 6843 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐โ๐ฅ) = (๐โ๐ฆ)) |
11 | 10 | oveq1d 7373 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐โ๐ฅ) ยทih ๐ง) = ((๐โ๐ฆ) ยทih ๐ง)) |
12 | 9, 11 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((๐ฅ ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ (๐ฆ ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง))) |
13 | 12 | cbvralvw 3224 |
. . . 4
โข
(โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง)) |
14 | 13 | ralbii 3093 |
. . 3
โข
(โ๐ง โ
โ โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ง)) = ((๐โ๐ฅ) ยทih ๐ง) โ โ๐ง โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง)) |
15 | | fveq2 6843 |
. . . . . . 7
โข (๐ง = ๐ฅ โ (๐โ๐ง) = (๐โ๐ฅ)) |
16 | 15 | oveq2d 7374 |
. . . . . 6
โข (๐ง = ๐ฅ โ (๐ฆ ยทih (๐โ๐ง)) = (๐ฆ ยทih (๐โ๐ฅ))) |
17 | | oveq2 7366 |
. . . . . 6
โข (๐ง = ๐ฅ โ ((๐โ๐ฆ) ยทih ๐ง) = ((๐โ๐ฆ) ยทih ๐ฅ)) |
18 | 16, 17 | eqeq12d 2749 |
. . . . 5
โข (๐ง = ๐ฅ โ ((๐ฆ ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง) โ (๐ฆ ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ))) |
19 | 18 | ralbidv 3171 |
. . . 4
โข (๐ง = ๐ฅ โ (โ๐ฆ โ โ (๐ฆ ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง) โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ))) |
20 | 19 | cbvralvw 3224 |
. . 3
โข
(โ๐ง โ
โ โ๐ฆ โ
โ (๐ฆ
ยทih (๐โ๐ง)) = ((๐โ๐ฆ) ยทih ๐ง) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ)) |
21 | 8, 14, 20 | 3bitri 297 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ)) |
22 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
โข ((๐: โโถ โ โง
๐ฆ โ โ) โ
(๐โ๐ฆ) โ โ) |
23 | | ax-his1 30066 |
. . . . . . . . . . . 12
โข (((๐โ๐ฆ) โ โ โง ๐ฅ โ โ) โ ((๐โ๐ฆ) ยทih ๐ฅ) = (โโ(๐ฅ
ยทih (๐โ๐ฆ)))) |
24 | 22, 23 | sylan 581 |
. . . . . . . . . . 11
โข (((๐: โโถ โ โง
๐ฆ โ โ) โง
๐ฅ โ โ) โ
((๐โ๐ฆ)
ยทih ๐ฅ) = (โโ(๐ฅ ยทih (๐โ๐ฆ)))) |
25 | 24 | adantrl 715 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐ฆ โ โ) โง
(๐: โโถ โ
โง ๐ฅ โ โ))
โ ((๐โ๐ฆ)
ยทih ๐ฅ) = (โโ(๐ฅ ยทih (๐โ๐ฆ)))) |
26 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
27 | | ax-his1 30066 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง (๐โ๐ฅ) โ โ) โ (๐ฆ ยทih (๐โ๐ฅ)) = (โโ((๐โ๐ฅ) ยทih ๐ฆ))) |
28 | 26, 27 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง (๐: โโถ โ โง
๐ฅ โ โ)) โ
(๐ฆ
ยทih (๐โ๐ฅ)) = (โโ((๐โ๐ฅ) ยทih ๐ฆ))) |
29 | 28 | adantll 713 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐ฆ โ โ) โง
(๐: โโถ โ
โง ๐ฅ โ โ))
โ (๐ฆ
ยทih (๐โ๐ฅ)) = (โโ((๐โ๐ฅ) ยทih ๐ฆ))) |
30 | 25, 29 | eqeq12d 2749 |
. . . . . . . . 9
โข (((๐: โโถ โ โง
๐ฆ โ โ) โง
(๐: โโถ โ
โง ๐ฅ โ โ))
โ (((๐โ๐ฆ)
ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)) โ (โโ(๐ฅ ยทih (๐โ๐ฆ))) = (โโ((๐โ๐ฅ) ยทih ๐ฆ)))) |
31 | 30 | ancoms 460 |
. . . . . . . 8
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
(๐: โโถ โ
โง ๐ฆ โ โ))
โ (((๐โ๐ฆ)
ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)) โ (โโ(๐ฅ ยทih (๐โ๐ฆ))) = (โโ((๐โ๐ฅ) ยทih ๐ฆ)))) |
32 | | hicl 30064 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โ (๐ฅ ยทih (๐โ๐ฆ)) โ โ) |
33 | 22, 32 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐: โโถ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทih (๐โ๐ฆ)) โ โ) |
34 | 33 | adantll 713 |
. . . . . . . . 9
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
(๐: โโถ โ
โง ๐ฆ โ โ))
โ (๐ฅ
ยทih (๐โ๐ฆ)) โ โ) |
35 | | hicl 30064 |
. . . . . . . . . . 11
โข (((๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฆ) โ
โ) |
36 | 26, 35 | sylan 581 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
๐ฆ โ โ) โ
((๐โ๐ฅ)
ยทih ๐ฆ) โ โ) |
37 | 36 | adantrl 715 |
. . . . . . . . 9
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
(๐: โโถ โ
โง ๐ฆ โ โ))
โ ((๐โ๐ฅ)
ยทih ๐ฆ) โ โ) |
38 | | cj11 15053 |
. . . . . . . . 9
โข (((๐ฅ
ยทih (๐โ๐ฆ)) โ โ โง ((๐โ๐ฅ) ยทih ๐ฆ) โ โ) โ
((โโ(๐ฅ
ยทih (๐โ๐ฆ))) = (โโ((๐โ๐ฅ) ยทih ๐ฆ)) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
39 | 34, 37, 38 | syl2anc 585 |
. . . . . . . 8
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
(๐: โโถ โ
โง ๐ฆ โ โ))
โ ((โโ(๐ฅ
ยทih (๐โ๐ฆ))) = (โโ((๐โ๐ฅ) ยทih ๐ฆ)) โ (๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
40 | 31, 39 | bitr2d 280 |
. . . . . . 7
โข (((๐: โโถ โ โง
๐ฅ โ โ) โง
(๐: โโถ โ
โง ๐ฆ โ โ))
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ ((๐โ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)))) |
41 | 40 | an4s 659 |
. . . . . 6
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ ((๐โ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)))) |
42 | 41 | anassrs 469 |
. . . . 5
โข ((((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โง ๐ฆ โ โ)
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ ((๐โ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)))) |
43 | | eqcom 2740 |
. . . . 5
โข (((๐โ๐ฆ) ยทih ๐ฅ) = (๐ฆ ยทih (๐โ๐ฅ)) โ (๐ฆ ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ)) |
44 | 42, 43 | bitrdi 287 |
. . . 4
โข ((((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โง ๐ฆ โ โ)
โ ((๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ (๐ฆ ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ))) |
45 | 44 | ralbidva 3169 |
. . 3
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ))) |
46 | 45 | ralbidva 3169 |
. 2
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฅ)) = ((๐โ๐ฆ) ยทih ๐ฅ))) |
47 | 21, 46 | bitr4id 290 |
1
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |