Step | Hyp | Ref
| Expression |
1 | | cnlnadj 31063 |
. . . . 5
โข (๐ฆ โ (LinOp โฉ ContOp)
โ โ๐ก โ
(LinOp โฉ ContOp)โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) |
2 | | df-rex 3071 |
. . . . 5
โข
(โ๐ก โ
(LinOp โฉ ContOp)โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)) โ โ๐ก(๐ก โ (LinOp โฉ ContOp) โง
โ๐ฅ โ โ
โ๐ง โ โ
((๐ฆโ๐ฅ)
ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)))) |
3 | 1, 2 | sylib 217 |
. . . 4
โข (๐ฆ โ (LinOp โฉ ContOp)
โ โ๐ก(๐ก โ (LinOp โฉ ContOp)
โง โ๐ฅ โ
โ โ๐ง โ
โ ((๐ฆโ๐ฅ)
ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)))) |
4 | | inss1 4189 |
. . . . . . . . . 10
โข (LinOp
โฉ ContOp) โ LinOp |
5 | 4 | sseli 3941 |
. . . . . . . . 9
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ๐ฆ โ
LinOp) |
6 | | lnopf 30843 |
. . . . . . . . 9
โข (๐ฆ โ LinOp โ ๐ฆ: โโถ
โ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ๐ฆ: โโถ
โ) |
8 | 7 | a1d 25 |
. . . . . . 7
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ((๐ก โ (LinOp
โฉ ContOp) โง โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ ๐ฆ: โโถ โ)) |
9 | 4 | sseli 3941 |
. . . . . . . . . 10
โข (๐ก โ (LinOp โฉ ContOp)
โ ๐ก โ
LinOp) |
10 | | lnopf 30843 |
. . . . . . . . . 10
โข (๐ก โ LinOp โ ๐ก: โโถ
โ) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
โข (๐ก โ (LinOp โฉ ContOp)
โ ๐ก: โโถ
โ) |
12 | 11 | a1i 11 |
. . . . . . . 8
โข (๐ฆ โ (LinOp โฉ ContOp)
โ (๐ก โ (LinOp
โฉ ContOp) โ ๐ก:
โโถ โ)) |
13 | 12 | adantrd 493 |
. . . . . . 7
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ((๐ก โ (LinOp
โฉ ContOp) โง โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ ๐ก: โโถ โ)) |
14 | | eqcom 2740 |
. . . . . . . . . . 11
โข (((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)) โ (๐ฅ ยทih (๐กโ๐ง)) = ((๐ฆโ๐ฅ) ยทih ๐ง)) |
15 | 14 | biimpi 215 |
. . . . . . . . . 10
โข (((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)) โ (๐ฅ ยทih (๐กโ๐ง)) = ((๐ฆโ๐ฅ) ยทih ๐ง)) |
16 | 15 | 2ralimi 3123 |
. . . . . . . . 9
โข
(โ๐ฅ โ
โ โ๐ง โ
โ ((๐ฆโ๐ฅ)
ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ ยทih (๐กโ๐ง)) = ((๐ฆโ๐ฅ) ยทih ๐ง)) |
17 | | adjsym 30817 |
. . . . . . . . . 10
โข ((๐ก: โโถ โ โง
๐ฆ: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ง โ
โ (๐ฅ
ยทih (๐กโ๐ง)) = ((๐ฆโ๐ฅ) ยทih ๐ง) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
18 | 11, 7, 17 | syl2anr 598 |
. . . . . . . . 9
โข ((๐ฆ โ (LinOp โฉ ContOp)
โง ๐ก โ (LinOp โฉ
ContOp)) โ (โ๐ฅ
โ โ โ๐ง
โ โ (๐ฅ
ยทih (๐กโ๐ง)) = ((๐ฆโ๐ฅ) ยทih ๐ง) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
19 | 16, 18 | imbitrid 243 |
. . . . . . . 8
โข ((๐ฆ โ (LinOp โฉ ContOp)
โง ๐ก โ (LinOp โฉ
ContOp)) โ (โ๐ฅ
โ โ โ๐ง
โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง)) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
20 | 19 | expimpd 455 |
. . . . . . 7
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ((๐ก โ (LinOp
โฉ ContOp) โง โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
21 | 8, 13, 20 | 3jcad 1130 |
. . . . . 6
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ((๐ก โ (LinOp
โฉ ContOp) โง โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ (๐ฆ: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง)))) |
22 | | dfadj2 30869 |
. . . . . . . 8
โข
adjโ = {โจ๐ข, ๐ฃโฉ โฃ (๐ข: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง))} |
23 | 22 | eleq2i 2826 |
. . . . . . 7
โข
(โจ๐ฆ, ๐กโฉ โ
adjโ โ โจ๐ฆ, ๐กโฉ โ {โจ๐ข, ๐ฃโฉ โฃ (๐ข: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง))}) |
24 | | vex 3448 |
. . . . . . . 8
โข ๐ฆ โ V |
25 | | vex 3448 |
. . . . . . . 8
โข ๐ก โ V |
26 | | feq1 6650 |
. . . . . . . . 9
โข (๐ข = ๐ฆ โ (๐ข: โโถ โ โ ๐ฆ: โโถ
โ)) |
27 | | fveq1 6842 |
. . . . . . . . . . . 12
โข (๐ข = ๐ฆ โ (๐ขโ๐ง) = (๐ฆโ๐ง)) |
28 | 27 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ข = ๐ฆ โ (๐ฅ ยทih (๐ขโ๐ง)) = (๐ฅ ยทih (๐ฆโ๐ง))) |
29 | 28 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ข = ๐ฆ โ ((๐ฅ ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง) โ (๐ฅ ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง))) |
30 | 29 | 2ralbidv 3209 |
. . . . . . . . 9
โข (๐ข = ๐ฆ โ (โ๐ฅ โ โ โ๐ง โ โ (๐ฅ ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง))) |
31 | 26, 30 | 3anbi13d 1439 |
. . . . . . . 8
โข (๐ข = ๐ฆ โ ((๐ข: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง)) โ (๐ฆ: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง)))) |
32 | | feq1 6650 |
. . . . . . . . 9
โข (๐ฃ = ๐ก โ (๐ฃ: โโถ โ โ ๐ก: โโถ
โ)) |
33 | | fveq1 6842 |
. . . . . . . . . . . 12
โข (๐ฃ = ๐ก โ (๐ฃโ๐ฅ) = (๐กโ๐ฅ)) |
34 | 33 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ก โ ((๐ฃโ๐ฅ) ยทih ๐ง) = ((๐กโ๐ฅ) ยทih ๐ง)) |
35 | 34 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ฃ = ๐ก โ ((๐ฅ ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง) โ (๐ฅ ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
36 | 35 | 2ralbidv 3209 |
. . . . . . . . 9
โข (๐ฃ = ๐ก โ (โ๐ฅ โ โ โ๐ง โ โ (๐ฅ ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง) โ โ๐ฅ โ โ โ๐ง โ โ (๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
37 | 32, 36 | 3anbi23d 1440 |
. . . . . . . 8
โข (๐ฃ = ๐ก โ ((๐ฆ: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง)) โ (๐ฆ: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง)))) |
38 | 24, 25, 31, 37 | opelopab 5500 |
. . . . . . 7
โข
(โจ๐ฆ, ๐กโฉ โ {โจ๐ข, ๐ฃโฉ โฃ (๐ข: โโถ โ โง ๐ฃ: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ขโ๐ง)) = ((๐ฃโ๐ฅ) ยทih ๐ง))} โ (๐ฆ: โโถ โ โง ๐ก: โโถ โ โง
โ๐ฅ โ โ
โ๐ง โ โ
(๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง))) |
39 | 23, 38 | bitr2i 276 |
. . . . . 6
โข ((๐ฆ: โโถ โ โง
๐ก: โโถ โ
โง โ๐ฅ โ
โ โ๐ง โ
โ (๐ฅ
ยทih (๐ฆโ๐ง)) = ((๐กโ๐ฅ) ยทih ๐ง)) โ โจ๐ฆ, ๐กโฉ โ
adjโ) |
40 | 21, 39 | syl6ib 251 |
. . . . 5
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ((๐ก โ (LinOp
โฉ ContOp) โง โ๐ฅ โ โ โ๐ง โ โ ((๐ฆโ๐ฅ) ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ โจ๐ฆ, ๐กโฉ โ
adjโ)) |
41 | 40 | eximdv 1921 |
. . . 4
โข (๐ฆ โ (LinOp โฉ ContOp)
โ (โ๐ก(๐ก โ (LinOp โฉ ContOp)
โง โ๐ฅ โ
โ โ๐ง โ
โ ((๐ฆโ๐ฅ)
ยทih ๐ง) = (๐ฅ ยทih (๐กโ๐ง))) โ โ๐กโจ๐ฆ, ๐กโฉ โ
adjโ)) |
42 | 3, 41 | mpd 15 |
. . 3
โข (๐ฆ โ (LinOp โฉ ContOp)
โ โ๐กโจ๐ฆ, ๐กโฉ โ
adjโ) |
43 | 24 | eldm2 5858 |
. . 3
โข (๐ฆ โ dom
adjโ โ โ๐กโจ๐ฆ, ๐กโฉ โ
adjโ) |
44 | 42, 43 | sylibr 233 |
. 2
โข (๐ฆ โ (LinOp โฉ ContOp)
โ ๐ฆ โ dom
adjโ) |
45 | 44 | ssriv 3949 |
1
โข (LinOp
โฉ ContOp) โ dom adjโ |