Step |
Hyp |
Ref |
Expression |
1 |
|
hgt750leme.o |
|- O = { z e. ZZ | -. 2 || z } |
2 |
|
hgt750leme.n |
|- ( ph -> N e. NN ) |
3 |
|
hgt750lemb.2 |
|- ( ph -> 2 <_ N ) |
4 |
|
hgt750lemb.a |
|- A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } |
5 |
|
hgt750lema.f |
|- F = ( d e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( d o. if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) ) ) |
6 |
|
fzofi |
|- ( 0 ..^ 3 ) e. Fin |
7 |
6
|
a1i |
|- ( ph -> ( 0 ..^ 3 ) e. Fin ) |
8 |
2
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
9 |
|
3nn0 |
|- 3 e. NN0 |
10 |
9
|
a1i |
|- ( ph -> 3 e. NN0 ) |
11 |
|
ssidd |
|- ( ph -> NN C_ NN ) |
12 |
8 10 11
|
reprfi2 |
|- ( ph -> ( NN ( repr ` 3 ) N ) e. Fin ) |
13 |
|
ssrab2 |
|- { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) |
14 |
13
|
a1i |
|- ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) ) |
15 |
12 14
|
ssfid |
|- ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } e. Fin ) |
16 |
15
|
adantr |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } e. Fin ) |
17 |
|
vmaf |
|- Lam : NN --> RR |
18 |
17
|
a1i |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR ) |
19 |
|
ssidd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> NN C_ NN ) |
20 |
8
|
nn0zd |
|- ( ph -> N e. ZZ ) |
21 |
20
|
ad2antrr |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> N e. ZZ ) |
22 |
9
|
a1i |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 3 e. NN0 ) |
23 |
|
simpr |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) |
24 |
13 23
|
sselid |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) ) |
25 |
19 21 22 24
|
reprf |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN ) |
26 |
|
c0ex |
|- 0 e. _V |
27 |
26
|
tpid1 |
|- 0 e. { 0 , 1 , 2 } |
28 |
|
fzo0to3tp |
|- ( 0 ..^ 3 ) = { 0 , 1 , 2 } |
29 |
27 28
|
eleqtrri |
|- 0 e. ( 0 ..^ 3 ) |
30 |
29
|
a1i |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) ) |
31 |
25 30
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN ) |
32 |
18 31
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR ) |
33 |
|
1ex |
|- 1 e. _V |
34 |
33
|
tpid2 |
|- 1 e. { 0 , 1 , 2 } |
35 |
34 28
|
eleqtrri |
|- 1 e. ( 0 ..^ 3 ) |
36 |
35
|
a1i |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) ) |
37 |
25 36
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN ) |
38 |
18 37
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR ) |
39 |
|
2ex |
|- 2 e. _V |
40 |
39
|
tpid3 |
|- 2 e. { 0 , 1 , 2 } |
41 |
40 28
|
eleqtrri |
|- 2 e. ( 0 ..^ 3 ) |
42 |
41
|
a1i |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) ) |
43 |
25 42
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN ) |
44 |
18 43
|
ffvelrnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR ) |
45 |
38 44
|
remulcld |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR ) |
46 |
32 45
|
remulcld |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
47 |
|
vmage0 |
|- ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) ) |
48 |
31 47
|
syl |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 0 ) ) ) |
49 |
|
vmage0 |
|- ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) ) |
50 |
37 49
|
syl |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 1 ) ) ) |
51 |
|
vmage0 |
|- ( ( n ` 2 ) e. NN -> 0 <_ ( Lam ` ( n ` 2 ) ) ) |
52 |
43 51
|
syl |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 2 ) ) ) |
53 |
38 44 50 52
|
mulge0d |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) |
54 |
32 45 48 53
|
mulge0d |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
55 |
7 16 46 54
|
fsumiunle |
|- ( ph -> sum_ n e. U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
56 |
|
eqid |
|- { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |
57 |
|
inss2 |
|- ( O i^i Prime ) C_ Prime |
58 |
|
prmssnn |
|- Prime C_ NN |
59 |
57 58
|
sstri |
|- ( O i^i Prime ) C_ NN |
60 |
59
|
a1i |
|- ( ph -> ( O i^i Prime ) C_ NN ) |
61 |
56 11 60 8 10
|
reprdifc |
|- ( ph -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) = U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) |
62 |
61
|
sumeq1d |
|- ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
63 |
|
ssrab2 |
|- { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) |
64 |
63
|
a1i |
|- ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) ) |
65 |
12 64
|
ssfid |
|- ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } e. Fin ) |
66 |
17
|
a1i |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR ) |
67 |
|
ssidd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> NN C_ NN ) |
68 |
20
|
adantr |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> N e. ZZ ) |
69 |
9
|
a1i |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 3 e. NN0 ) |
70 |
64
|
sselda |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) ) |
71 |
67 68 69 70
|
reprf |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN ) |
72 |
29
|
a1i |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) ) |
73 |
71 72
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN ) |
74 |
66 73
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR ) |
75 |
35
|
a1i |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) ) |
76 |
71 75
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN ) |
77 |
66 76
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR ) |
78 |
41
|
a1i |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) ) |
79 |
71 78
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN ) |
80 |
66 79
|
ffvelrnd |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR ) |
81 |
77 80
|
remulcld |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR ) |
82 |
74 81
|
remulcld |
|- ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
83 |
65 82
|
fsumrecl |
|- ( ph -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
84 |
83
|
recnd |
|- ( ph -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC ) |
85 |
|
fsumconst |
|- ( ( ( 0 ..^ 3 ) e. Fin /\ sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC ) -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) |
86 |
7 84 85
|
syl2anc |
|- ( ph -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) |
87 |
|
fveq1 |
|- ( n = ( F ` e ) -> ( n ` 0 ) = ( ( F ` e ) ` 0 ) ) |
88 |
87
|
fveq2d |
|- ( n = ( F ` e ) -> ( Lam ` ( n ` 0 ) ) = ( Lam ` ( ( F ` e ) ` 0 ) ) ) |
89 |
|
fveq1 |
|- ( n = ( F ` e ) -> ( n ` 1 ) = ( ( F ` e ) ` 1 ) ) |
90 |
89
|
fveq2d |
|- ( n = ( F ` e ) -> ( Lam ` ( n ` 1 ) ) = ( Lam ` ( ( F ` e ) ` 1 ) ) ) |
91 |
|
fveq1 |
|- ( n = ( F ` e ) -> ( n ` 2 ) = ( ( F ` e ) ` 2 ) ) |
92 |
91
|
fveq2d |
|- ( n = ( F ` e ) -> ( Lam ` ( n ` 2 ) ) = ( Lam ` ( ( F ` e ) ` 2 ) ) ) |
93 |
90 92
|
oveq12d |
|- ( n = ( F ` e ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) = ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) |
94 |
88 93
|
oveq12d |
|- ( n = ( F ` e ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) ) |
95 |
|
3nn |
|- 3 e. NN |
96 |
95
|
a1i |
|- ( ph -> 3 e. NN ) |
97 |
96
|
ralrimivw |
|- ( ph -> A. a e. ( 0 ..^ 3 ) 3 e. NN ) |
98 |
97
|
r19.21bi |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> 3 e. NN ) |
99 |
20
|
adantr |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> N e. ZZ ) |
100 |
|
ssidd |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> NN C_ NN ) |
101 |
|
simpr |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> a e. ( 0 ..^ 3 ) ) |
102 |
|
fveq1 |
|- ( c = d -> ( c ` 0 ) = ( d ` 0 ) ) |
103 |
102
|
eleq1d |
|- ( c = d -> ( ( c ` 0 ) e. ( O i^i Prime ) <-> ( d ` 0 ) e. ( O i^i Prime ) ) ) |
104 |
103
|
notbid |
|- ( c = d -> ( -. ( c ` 0 ) e. ( O i^i Prime ) <-> -. ( d ` 0 ) e. ( O i^i Prime ) ) ) |
105 |
104
|
cbvrabv |
|- { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } = { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } |
106 |
|
fveq1 |
|- ( c = d -> ( c ` a ) = ( d ` a ) ) |
107 |
106
|
eleq1d |
|- ( c = d -> ( ( c ` a ) e. ( O i^i Prime ) <-> ( d ` a ) e. ( O i^i Prime ) ) ) |
108 |
107
|
notbid |
|- ( c = d -> ( -. ( c ` a ) e. ( O i^i Prime ) <-> -. ( d ` a ) e. ( O i^i Prime ) ) ) |
109 |
108
|
cbvrabv |
|- { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } = { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` a ) e. ( O i^i Prime ) } |
110 |
|
eqid |
|- if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) = if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) |
111 |
98 99 100 101 105 109 110 5
|
reprpmtf1o |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> F : { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } -1-1-onto-> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) |
112 |
|
eqidd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( F ` e ) = ( F ` e ) ) |
113 |
82
|
adantlr |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
114 |
113
|
recnd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC ) |
115 |
94 16 111 112 114
|
fsumf1o |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) ) |
116 |
|
fveq2 |
|- ( e = n -> ( F ` e ) = ( F ` n ) ) |
117 |
116
|
fveq1d |
|- ( e = n -> ( ( F ` e ) ` 0 ) = ( ( F ` n ) ` 0 ) ) |
118 |
117
|
fveq2d |
|- ( e = n -> ( Lam ` ( ( F ` e ) ` 0 ) ) = ( Lam ` ( ( F ` n ) ` 0 ) ) ) |
119 |
116
|
fveq1d |
|- ( e = n -> ( ( F ` e ) ` 1 ) = ( ( F ` n ) ` 1 ) ) |
120 |
119
|
fveq2d |
|- ( e = n -> ( Lam ` ( ( F ` e ) ` 1 ) ) = ( Lam ` ( ( F ` n ) ` 1 ) ) ) |
121 |
116
|
fveq1d |
|- ( e = n -> ( ( F ` e ) ` 2 ) = ( ( F ` n ) ` 2 ) ) |
122 |
121
|
fveq2d |
|- ( e = n -> ( Lam ` ( ( F ` e ) ` 2 ) ) = ( Lam ` ( ( F ` n ) ` 2 ) ) ) |
123 |
120 122
|
oveq12d |
|- ( e = n -> ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) = ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) |
124 |
118 123
|
oveq12d |
|- ( e = n -> ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) ) |
125 |
124
|
cbvsumv |
|- sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) |
126 |
125
|
a1i |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) ) |
127 |
|
ovexd |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( 0 ..^ 3 ) e. _V ) |
128 |
101
|
adantr |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> a e. ( 0 ..^ 3 ) ) |
129 |
127 128 30 110
|
pmtridf1o |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) ) |
130 |
5 129 25 18 23
|
hgt750lemg |
|- ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
131 |
130
|
sumeq2dv |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
132 |
115 126 131
|
3eqtrrd |
|- ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
133 |
132
|
sumeq2dv |
|- ( ph -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
134 |
|
hashfzo0 |
|- ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 ) |
135 |
9 134
|
ax-mp |
|- ( # ` ( 0 ..^ 3 ) ) = 3 |
136 |
135
|
a1i |
|- ( ph -> ( # ` ( 0 ..^ 3 ) ) = 3 ) |
137 |
136
|
eqcomd |
|- ( ph -> 3 = ( # ` ( 0 ..^ 3 ) ) ) |
138 |
4
|
a1i |
|- ( ph -> A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) |
139 |
138
|
sumeq1d |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
140 |
137 139
|
oveq12d |
|- ( ph -> ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) |
141 |
86 133 140
|
3eqtr4rd |
|- ( ph -> ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) |
142 |
55 62 141
|
3brtr4d |
|- ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) |