Step | Hyp | Ref
| Expression |
1 | | dmadjrn 30666 |
. . 3
โข (๐ โ dom
adjโ โ (adjโโ๐) โ dom
adjโ) |
2 | | dmadjop 30659 |
. . 3
โข
((adjโโ๐) โ dom adjโ โ
(adjโโ๐): โโถ โ) |
3 | 1, 2 | syl 17 |
. 2
โข (๐ โ dom
adjโ โ (adjโโ๐): โโถ โ) |
4 | | simp2 1137 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ๐ค โ โ) |
5 | | adjcl 30703 |
. . . . . . . . . . . . . . 15
โข ((๐ โ dom
adjโ โง ๐ฆ โ โ) โ
((adjโโ๐)โ๐ฆ) โ โ) |
6 | | hvmulcl 29784 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ (๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) โ โ) |
7 | 5, 6 | sylan2 593 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐ โ dom
adjโ โง ๐ฆ โ โ)) โ (๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) โ โ) |
8 | 7 | an12s 647 |
. . . . . . . . . . . . 13
โข ((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) โ โ) |
9 | 8 | adantrr 715 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) โ โ) |
10 | 9 | 3adant2 1131 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) โ โ) |
11 | | adjcl 30703 |
. . . . . . . . . . . . 13
โข ((๐ โ dom
adjโ โง ๐ง โ โ) โ
((adjโโ๐)โ๐ง) โ โ) |
12 | 11 | adantrl 714 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ
((adjโโ๐)โ๐ง) โ โ) |
13 | 12 | 3adant2 1131 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ
((adjโโ๐)โ๐ง) โ โ) |
14 | | his7 29861 |
. . . . . . . . . . 11
โข ((๐ค โ โ โง (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) โ โ โง
((adjโโ๐)โ๐ง) โ โ) โ (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) = ((๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ))) + (๐ค ยทih
((adjโโ๐)โ๐ง)))) |
15 | 4, 10, 13, 14 | syl3anc 1371 |
. . . . . . . . . 10
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) = ((๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ))) + (๐ค ยทih
((adjโโ๐)โ๐ง)))) |
16 | | adj2 30705 |
. . . . . . . . . . . . . . 15
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ๐ฆ โ โ) โ ((๐โ๐ค) ยทih ๐ฆ) = (๐ค ยทih
((adjโโ๐)โ๐ฆ))) |
17 | 16 | 3adant3l 1180 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ค) ยทih ๐ฆ) = (๐ค ยทih
((adjโโ๐)โ๐ฆ))) |
18 | 17 | oveq2d 7367 |
. . . . . . . . . . . . 13
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((โโ๐ฅ)
ยท ((๐โ๐ค)
ยทih ๐ฆ)) = ((โโ๐ฅ) ยท (๐ค ยทih
((adjโโ๐)โ๐ฆ)))) |
19 | | simp3l 1201 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ โ) |
20 | | dmadjop 30659 |
. . . . . . . . . . . . . . . 16
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
21 | 20 | ffvelcdmda 7031 |
. . . . . . . . . . . . . . 15
โข ((๐ โ dom
adjโ โง ๐ค โ โ) โ (๐โ๐ค) โ โ) |
22 | 21 | 3adant3 1132 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐โ๐ค) โ โ) |
23 | | simp3r 1202 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฆ โ โ) |
24 | | his5 29857 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (๐โ๐ค) โ โ โง ๐ฆ โ โ) โ ((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) = ((โโ๐ฅ) ยท ((๐โ๐ค) ยทih ๐ฆ))) |
25 | 19, 22, 23, 24 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) = ((โโ๐ฅ) ยท ((๐โ๐ค) ยทih ๐ฆ))) |
26 | | simp2 1137 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ค โ โ) |
27 | 5 | adantrl 714 |
. . . . . . . . . . . . . . 15
โข ((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((adjโโ๐)โ๐ฆ) โ โ) |
28 | 27 | 3adant2 1131 |
. . . . . . . . . . . . . 14
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((adjโโ๐)โ๐ฆ) โ โ) |
29 | | his5 29857 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ค โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ (๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ))) = ((โโ๐ฅ) ยท (๐ค ยทih
((adjโโ๐)โ๐ฆ)))) |
30 | 19, 26, 28, 29 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ))) = ((โโ๐ฅ) ยท (๐ค ยทih
((adjโโ๐)โ๐ฆ)))) |
31 | 18, 25, 30 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) = (๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)))) |
32 | 31 | 3adant3r 1181 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) = (๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)))) |
33 | | adj2 30705 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ๐ง โ โ) โ ((๐โ๐ค) ยทih ๐ง) = (๐ค ยทih
((adjโโ๐)โ๐ง))) |
34 | 33 | 3adant3l 1180 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐โ๐ค) ยทih ๐ง) = (๐ค ยทih
((adjโโ๐)โ๐ง))) |
35 | 32, 34 | oveq12d 7369 |
. . . . . . . . . 10
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) + ((๐โ๐ค) ยทih ๐ง)) = ((๐ค ยทih (๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ))) + (๐ค ยทih
((adjโโ๐)โ๐ง)))) |
36 | 21 | 3adant3 1132 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐โ๐ค) โ โ) |
37 | | hvmulcl 29784 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
39 | 38 | 3ad2ant3 1135 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ฅ ยทโ ๐ฆ) โ
โ) |
40 | | simp3r 1202 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ๐ง โ โ) |
41 | | his7 29861 |
. . . . . . . . . . . 12
โข (((๐โ๐ค) โ โ โง (๐ฅ ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐โ๐ค) ยทih ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = (((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) + ((๐โ๐ค) ยทih ๐ง))) |
42 | 36, 39, 40, 41 | syl3anc 1371 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐โ๐ค) ยทih ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = (((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) + ((๐โ๐ค) ยทih ๐ง))) |
43 | | hvaddcl 29783 |
. . . . . . . . . . . . 13
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ
โ) |
44 | 37, 43 | sylan 580 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
45 | | adj2 30705 |
. . . . . . . . . . . 12
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ โ) โ ((๐โ๐ค) ยทih ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
46 | 44, 45 | syl3an3 1165 |
. . . . . . . . . . 11
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐โ๐ค) ยทih ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
47 | 42, 46 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (((๐โ๐ค) ยทih (๐ฅ
ยทโ ๐ฆ)) + ((๐โ๐ค) ยทih ๐ง)) = (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
48 | 15, 35, 47 | 3eqtr2rd 2784 |
. . . . . . . . 9
โข ((๐ โ dom
adjโ โง ๐ค โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
49 | 48 | 3com23 1126 |
. . . . . . . 8
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ๐ค โ โ) โ (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
50 | 49 | 3expa 1118 |
. . . . . . 7
โข (((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โง ๐ค โ โ) โ (๐ค ยทih
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
51 | 50 | ralrimiva 3141 |
. . . . . 6
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ โ๐ค โ โ (๐ค
ยทih ((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
52 | | adjcl 30703 |
. . . . . . . 8
โข ((๐ โ dom
adjโ โง ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ โ) โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) โ
โ) |
53 | 44, 52 | sylan2 593 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) โ
โ) |
54 | | hvaddcl 29783 |
. . . . . . . . 9
โข (((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) โ โ โง
((adjโโ๐)โ๐ง) โ โ) โ ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)) โ โ) |
55 | 8, 11, 54 | syl2an 596 |
. . . . . . . 8
โข (((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ โ dom adjโ โง
๐ง โ โ)) โ
((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)) โ โ) |
56 | 55 | anandis 676 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)) โ โ) |
57 | | hial2eq2 29878 |
. . . . . . 7
โข
((((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) โ โ โง ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)) โ โ) โ (โ๐ค โ โ (๐ค
ยทih ((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
58 | 53, 56, 57 | syl2anc 584 |
. . . . . 6
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (โ๐ค โ โ (๐ค
ยทih ((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ค ยทih ((๐ฅ
ยทโ ((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
59 | 51, 58 | mpbid 231 |
. . . . 5
โข ((๐ โ dom
adjโ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) |
60 | 59 | exp32 421 |
. . . 4
โข (๐ โ dom
adjโ โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ง โ โ โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))))) |
61 | 60 | ralrimdv 3147 |
. . 3
โข (๐ โ dom
adjโ โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ โ๐ง โ โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
62 | 61 | ralrimivv 3193 |
. 2
โข (๐ โ dom
adjโ โ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง))) |
63 | | ellnop 30629 |
. 2
โข
((adjโโ๐) โ LinOp โ
((adjโโ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
((adjโโ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ
((adjโโ๐)โ๐ฆ)) +โ
((adjโโ๐)โ๐ง)))) |
64 | 3, 62, 63 | sylanbrc 583 |
1
โข (๐ โ dom
adjโ โ (adjโโ๐) โ LinOp) |