Step |
Hyp |
Ref |
Expression |
1 |
|
vmaval.1 |
|- S = { p e. Prime | p || A } |
2 |
|
prmex |
|- Prime e. _V |
3 |
2
|
rabex |
|- { p e. Prime | p || x } e. _V |
4 |
3
|
a1i |
|- ( x = A -> { p e. Prime | p || x } e. _V ) |
5 |
|
id |
|- ( s = { p e. Prime | p || x } -> s = { p e. Prime | p || x } ) |
6 |
|
breq2 |
|- ( x = A -> ( p || x <-> p || A ) ) |
7 |
6
|
rabbidv |
|- ( x = A -> { p e. Prime | p || x } = { p e. Prime | p || A } ) |
8 |
7 1
|
eqtr4di |
|- ( x = A -> { p e. Prime | p || x } = S ) |
9 |
5 8
|
sylan9eqr |
|- ( ( x = A /\ s = { p e. Prime | p || x } ) -> s = S ) |
10 |
9
|
fveqeq2d |
|- ( ( x = A /\ s = { p e. Prime | p || x } ) -> ( ( # ` s ) = 1 <-> ( # ` S ) = 1 ) ) |
11 |
9
|
unieqd |
|- ( ( x = A /\ s = { p e. Prime | p || x } ) -> U. s = U. S ) |
12 |
11
|
fveq2d |
|- ( ( x = A /\ s = { p e. Prime | p || x } ) -> ( log ` U. s ) = ( log ` U. S ) ) |
13 |
10 12
|
ifbieq1d |
|- ( ( x = A /\ s = { p e. Prime | p || x } ) -> if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) ) |
14 |
4 13
|
csbied |
|- ( x = A -> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) ) |
15 |
|
df-vma |
|- Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) ) |
16 |
|
fvex |
|- ( log ` U. S ) e. _V |
17 |
|
c0ex |
|- 0 e. _V |
18 |
16 17
|
ifex |
|- if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) e. _V |
19 |
14 15 18
|
fvmpt |
|- ( A e. NN -> ( Lam ` A ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) ) |