# 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
rrx0el.p ${⊢}{P}={ℝ}^{{I}}$
Assertion rrx0el

### Proof

Step Hyp Ref Expression
1 rrx0el.0
2 rrx0el.p ${⊢}{P}={ℝ}^{{I}}$
3 c0ex ${⊢}0\in \mathrm{V}$
4 3 fconst ${⊢}\left({I}×\left\{0\right\}\right):{I}⟶\left\{0\right\}$
5 4 a1i ${⊢}{I}\in {V}\to \left({I}×\left\{0\right\}\right):{I}⟶\left\{0\right\}$
6 0re ${⊢}0\in ℝ$
7 snssg ${⊢}0\in ℝ\to \left(0\in ℝ↔\left\{0\right\}\subseteq ℝ\right)$
8 6 7 ax-mp ${⊢}0\in ℝ↔\left\{0\right\}\subseteq ℝ$
9 6 8 mpbi ${⊢}\left\{0\right\}\subseteq ℝ$
10 9 a1i ${⊢}{I}\in {V}\to \left\{0\right\}\subseteq ℝ$
11 5 10 fssd ${⊢}{I}\in {V}\to \left({I}×\left\{0\right\}\right):{I}⟶ℝ$
12 reex ${⊢}ℝ\in \mathrm{V}$
13 12 a1i ${⊢}{I}\in {V}\to ℝ\in \mathrm{V}$
14 id ${⊢}{I}\in {V}\to {I}\in {V}$
15 13 14 elmapd ${⊢}{I}\in {V}\to \left({I}×\left\{0\right\}\in \left({ℝ}^{{I}}\right)↔\left({I}×\left\{0\right\}\right):{I}⟶ℝ\right)$
16 11 15 mpbird ${⊢}{I}\in {V}\to {I}×\left\{0\right\}\in \left({ℝ}^{{I}}\right)$
17 16 1 2 3eltr4g