Step | Hyp | Ref
| Expression |
1 | | cnlnadjlem.5 |
. . 3
โข ๐น = (๐ฆ โ โ โฆ ๐ต) |
2 | | cnlnadjlem.1 |
. . . 4
โข ๐ โ LinOp |
3 | | cnlnadjlem.2 |
. . . 4
โข ๐ โ ContOp |
4 | | cnlnadjlem.3 |
. . . 4
โข ๐บ = (๐ โ โ โฆ ((๐โ๐) ยทih ๐ฆ)) |
5 | | cnlnadjlem.4 |
. . . 4
โข ๐ต = (โฉ๐ค โ โ โ๐ฃ โ โ ((๐โ๐ฃ) ยทih ๐ฆ) = (๐ฃ ยทih ๐ค)) |
6 | 2, 3, 4, 5 | cnlnadjlem3 31060 |
. . 3
โข (๐ฆ โ โ โ ๐ต โ
โ) |
7 | 1, 6 | fmpti 7064 |
. 2
โข ๐น: โโถ
โ |
8 | 2 | lnopfi 30960 |
. . . . . . . . . 10
โข ๐: โโถ
โ |
9 | 8 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ก โ โ โ (๐โ๐ก) โ โ) |
10 | 9 | adantl 483 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐โ๐ก) โ โ) |
11 | | hvmulcl 30004 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ
ยทโ ๐) โ โ) |
12 | 11 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐ฅ
ยทโ ๐) โ โ) |
13 | | simplr 768 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ๐ง โ
โ) |
14 | | his7 30081 |
. . . . . . . 8
โข (((๐โ๐ก) โ โ โง (๐ฅ ยทโ ๐) โ โ โง ๐ง โ โ) โ ((๐โ๐ก) ยทih ((๐ฅ
ยทโ ๐) +โ ๐ง)) = (((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) + ((๐โ๐ก) ยทih ๐ง))) |
15 | 10, 12, 13, 14 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ((๐ฅ
ยทโ ๐) +โ ๐ง)) = (((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) + ((๐โ๐ก) ยทih ๐ง))) |
16 | | hvaddcl 30003 |
. . . . . . . . 9
โข (((๐ฅ
ยทโ ๐) โ โ โง ๐ง โ โ) โ ((๐ฅ ยทโ ๐) +โ ๐ง) โ
โ) |
17 | 11, 16 | sylan 581 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐) +โ ๐ง) โ โ) |
18 | 2, 3, 4, 5, 1 | cnlnadjlem5 31062 |
. . . . . . . 8
โข ((((๐ฅ
ยทโ ๐) +โ ๐ง) โ โ โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ((๐ฅ
ยทโ ๐) +โ ๐ง)) = (๐ก ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)))) |
19 | 17, 18 | sylan 581 |
. . . . . . 7
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ((๐ฅ
ยทโ ๐) +โ ๐ง)) = (๐ก ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)))) |
20 | | simpll 766 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ๐ฅ โ
โ) |
21 | 9 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ (๐โ๐ก) โ โ) |
22 | | simplr 768 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ๐ โ
โ) |
23 | | his5 30077 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง (๐โ๐ก) โ โ โง ๐ โ โ) โ ((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) = ((โโ๐ฅ) ยท ((๐โ๐ก) ยทih ๐))) |
24 | 20, 21, 22, 23 | syl3anc 1372 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) = ((โโ๐ฅ) ยท ((๐โ๐ก) ยทih ๐))) |
25 | | simpr 486 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ๐ก โ
โ) |
26 | 2, 3, 4, 5, 1 | cnlnadjlem4 31061 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐นโ๐) โ โ) |
27 | 26 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ (๐นโ๐) โ โ) |
28 | | his5 30077 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ก โ โ โง (๐นโ๐) โ โ) โ (๐ก ยทih (๐ฅ
ยทโ (๐นโ๐))) = ((โโ๐ฅ) ยท (๐ก ยทih (๐นโ๐)))) |
29 | 20, 25, 27, 28 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ (๐ก
ยทih (๐ฅ ยทโ (๐นโ๐))) = ((โโ๐ฅ) ยท (๐ก ยทih (๐นโ๐)))) |
30 | 2, 3, 4, 5, 1 | cnlnadjlem5 31062 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ๐) = (๐ก ยทih (๐นโ๐))) |
31 | 30 | adantll 713 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ๐) = (๐ก ยทih (๐นโ๐))) |
32 | 31 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ
((โโ๐ฅ)
ยท ((๐โ๐ก)
ยทih ๐)) = ((โโ๐ฅ) ยท (๐ก ยทih (๐นโ๐)))) |
33 | 29, 32 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ (๐ก
ยทih (๐ฅ ยทโ (๐นโ๐))) = ((โโ๐ฅ) ยท ((๐โ๐ก) ยทih ๐))) |
34 | 24, 33 | eqtr4d 2776 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) = (๐ก ยทih (๐ฅ
ยทโ (๐นโ๐)))) |
35 | 34 | adantlr 714 |
. . . . . . . . 9
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) = (๐ก ยทih (๐ฅ
ยทโ (๐นโ๐)))) |
36 | 2, 3, 4, 5, 1 | cnlnadjlem5 31062 |
. . . . . . . . . 10
โข ((๐ง โ โ โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ๐ง) = (๐ก ยทih (๐นโ๐ง))) |
37 | 36 | adantll 713 |
. . . . . . . . 9
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ((๐โ๐ก) ยทih ๐ง) = (๐ก ยทih (๐นโ๐ง))) |
38 | 35, 37 | oveq12d 7379 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) + ((๐โ๐ก) ยทih ๐ง)) = ((๐ก ยทih (๐ฅ
ยทโ (๐นโ๐))) + (๐ก ยทih (๐นโ๐ง)))) |
39 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ ๐ก โ
โ) |
40 | | hvmulcl 30004 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐นโ๐) โ โ) โ (๐ฅ ยทโ (๐นโ๐)) โ โ) |
41 | 26, 40 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ
ยทโ (๐นโ๐)) โ โ) |
42 | 41 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐ฅ
ยทโ (๐นโ๐)) โ โ) |
43 | 2, 3, 4, 5, 1 | cnlnadjlem4 31061 |
. . . . . . . . . 10
โข (๐ง โ โ โ (๐นโ๐ง) โ โ) |
44 | 43 | ad2antlr 726 |
. . . . . . . . 9
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐นโ๐ง) โ โ) |
45 | | his7 30081 |
. . . . . . . . 9
โข ((๐ก โ โ โง (๐ฅ
ยทโ (๐นโ๐)) โ โ โง (๐นโ๐ง) โ โ) โ (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) = ((๐ก ยทih (๐ฅ
ยทโ (๐นโ๐))) + (๐ก ยทih (๐นโ๐ง)))) |
46 | 39, 42, 44, 45 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐ก
ยทih ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) = ((๐ก ยทih (๐ฅ
ยทโ (๐นโ๐))) + (๐ก ยทih (๐นโ๐ง)))) |
47 | 38, 46 | eqtr4d 2776 |
. . . . . . 7
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (((๐โ๐ก) ยทih (๐ฅ
ยทโ ๐)) + ((๐โ๐ก) ยทih ๐ง)) = (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
48 | 15, 19, 47 | 3eqtr3d 2781 |
. . . . . 6
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โง ๐ก โ โ) โ (๐ก
ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง))) = (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
49 | 48 | ralrimiva 3140 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ
โ๐ก โ โ
(๐ก
ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง))) = (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
50 | 2, 3, 4, 5, 1 | cnlnadjlem4 31061 |
. . . . . . 7
โข (((๐ฅ
ยทโ ๐) +โ ๐ง) โ โ โ (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) โ
โ) |
51 | 17, 50 | syl 17 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) โ
โ) |
52 | | hvaddcl 30003 |
. . . . . . 7
โข (((๐ฅ
ยทโ (๐นโ๐)) โ โ โง (๐นโ๐ง) โ โ) โ ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง)) โ โ) |
53 | 41, 43, 52 | syl2an 597 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง)) โ โ) |
54 | | hial2eq2 30098 |
. . . . . 6
โข (((๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) โ โ โง ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง)) โ โ) โ (โ๐ก โ โ (๐ก
ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง))) = (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) โ (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
55 | 51, 53, 54 | syl2anc 585 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ
(โ๐ก โ โ
(๐ก
ยทih (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง))) = (๐ก ยทih ((๐ฅ
ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) โ (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
56 | 49, 55 | mpbid 231 |
. . . 4
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ง โ โ) โ (๐นโ((๐ฅ ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) |
57 | 56 | ralrimiva 3140 |
. . 3
โข ((๐ฅ โ โ โง ๐ โ โ) โ
โ๐ง โ โ
(๐นโ((๐ฅ
ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง))) |
58 | 57 | rgen2 3191 |
. 2
โข
โ๐ฅ โ
โ โ๐ โ
โ โ๐ง โ
โ (๐นโ((๐ฅ
ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง)) |
59 | | ellnop 30849 |
. 2
โข (๐น โ LinOp โ (๐น: โโถ โ โง
โ๐ฅ โ โ
โ๐ โ โ
โ๐ง โ โ
(๐นโ((๐ฅ
ยทโ ๐) +โ ๐ง)) = ((๐ฅ ยทโ (๐นโ๐)) +โ (๐นโ๐ง)))) |
60 | 7, 58, 59 | mpbir2an 710 |
1
โข ๐น โ LinOp |