Metamath Proof Explorer

Theorem blssp

Description: A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypothesis blssp.2 
|- N = ( M |` ( S X. S ) )
Assertion blssp 
|- ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> ( Y ( ball ` N ) R ) = ( ( Y ( ball ` M ) R ) i^i S ) )

Proof

Step Hyp Ref Expression
1 blssp.2 
 |-  N = ( M |` ( S X. S ) )
2 metxmet 
 |-  ( M e. ( Met ` X ) -> M e. ( *Met ` X ) )
3 2 ad2antrr 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> M e. ( *Met ` X ) )
4 simprl 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> Y e. S )
5 simplr 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> S C_ X )
6 sseqin2 
 |-  ( S C_ X <-> ( X i^i S ) = S )
7 5 6 sylib 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> ( X i^i S ) = S )
8 4 7 eleqtrrd 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> Y e. ( X i^i S ) )
9 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
10 9 ad2antll 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> R e. RR* )
11 1 blres 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. ( X i^i S ) /\ R e. RR* ) -> ( Y ( ball ` N ) R ) = ( ( Y ( ball ` M ) R ) i^i S ) )
12 3 8 10 11 syl3anc 
 |-  ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> ( Y ( ball ` N ) R ) = ( ( Y ( ball ` M ) R ) i^i S ) )