This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrx0el

Description: The zero ("origin") in a generalized real Euclidean space is an element of its base set. (Contributed by AV, 11-Feb-2023)

Ref Expression
Hypotheses rrx0el.0 
|- .0. = ( I X. { 0 } )
rrx0el.p 
|- P = ( RR ^m I )
Assertion rrx0el 
|- ( I e. V -> .0. e. P )

Proof

Step Hyp Ref Expression
1 rrx0el.0 
 |-  .0. = ( I X. { 0 } )
2 rrx0el.p 
 |-  P = ( RR ^m I )
3 c0ex 
 |-  0 e. _V
4 3 fconst 
 |-  ( I X. { 0 } ) : I --> { 0 }
5 4 a1i 
 |-  ( I e. V -> ( I X. { 0 } ) : I --> { 0 } )
6 0re 
 |-  0 e. RR
7 snssg 
 |-  ( 0 e. RR -> ( 0 e. RR <-> { 0 } C_ RR ) )
8 6 7 ax-mp 
 |-  ( 0 e. RR <-> { 0 } C_ RR )
9 6 8 mpbi 
 |-  { 0 } C_ RR
10 9 a1i 
 |-  ( I e. V -> { 0 } C_ RR )
11 5 10 fssd 
 |-  ( I e. V -> ( I X. { 0 } ) : I --> RR )
12 reex 
 |-  RR e. _V
13 12 a1i 
 |-  ( I e. V -> RR e. _V )
14 id 
 |-  ( I e. V -> I e. V )
15 13 14 elmapd 
 |-  ( I e. V -> ( ( I X. { 0 } ) e. ( RR ^m I ) <-> ( I X. { 0 } ) : I --> RR ) )
16 11 15 mpbird 
 |-  ( I e. V -> ( I X. { 0 } ) e. ( RR ^m I ) )
17 16 1 2 3eltr4g 
 |-  ( I e. V -> .0. e. P )