rrx0el

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

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

Metamath Proof Explorer