Step |
Hyp |
Ref |
Expression |
1 |
|
carsgval.1 |
|- ( ph -> O e. V ) |
2 |
|
carsgval.2 |
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) ) |
3 |
|
baselcarsg.1 |
|- ( ph -> ( M ` (/) ) = 0 ) |
4 |
|
ssidd |
|- ( ph -> O C_ O ) |
5 |
|
elpwi |
|- ( e e. ~P O -> e C_ O ) |
6 |
5
|
adantl |
|- ( ( ph /\ e e. ~P O ) -> e C_ O ) |
7 |
|
df-ss |
|- ( e C_ O <-> ( e i^i O ) = e ) |
8 |
6 7
|
sylib |
|- ( ( ph /\ e e. ~P O ) -> ( e i^i O ) = e ) |
9 |
8
|
fveq2d |
|- ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i O ) ) = ( M ` e ) ) |
10 |
|
ssdif0 |
|- ( e C_ O <-> ( e \ O ) = (/) ) |
11 |
6 10
|
sylib |
|- ( ( ph /\ e e. ~P O ) -> ( e \ O ) = (/) ) |
12 |
11
|
fveq2d |
|- ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ O ) ) = ( M ` (/) ) ) |
13 |
3
|
adantr |
|- ( ( ph /\ e e. ~P O ) -> ( M ` (/) ) = 0 ) |
14 |
12 13
|
eqtrd |
|- ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ O ) ) = 0 ) |
15 |
9 14
|
oveq12d |
|- ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( ( M ` e ) +e 0 ) ) |
16 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
17 |
2
|
adantr |
|- ( ( ph /\ e e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) ) |
18 |
|
simpr |
|- ( ( ph /\ e e. ~P O ) -> e e. ~P O ) |
19 |
17 18
|
ffvelrnd |
|- ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) ) |
20 |
16 19
|
sselid |
|- ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* ) |
21 |
|
xaddid1 |
|- ( ( M ` e ) e. RR* -> ( ( M ` e ) +e 0 ) = ( M ` e ) ) |
22 |
20 21
|
syl |
|- ( ( ph /\ e e. ~P O ) -> ( ( M ` e ) +e 0 ) = ( M ` e ) ) |
23 |
15 22
|
eqtrd |
|- ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) |
24 |
23
|
ralrimiva |
|- ( ph -> A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) |
25 |
4 24
|
jca |
|- ( ph -> ( O C_ O /\ A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) ) |
26 |
1 2
|
elcarsg |
|- ( ph -> ( O e. ( toCaraSiga ` M ) <-> ( O C_ O /\ A. e e. ~P O ( ( M ` ( e i^i O ) ) +e ( M ` ( e \ O ) ) ) = ( M ` e ) ) ) ) |
27 |
25 26
|
mpbird |
|- ( ph -> O e. ( toCaraSiga ` M ) ) |