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 )