Theorem rrx0

Description: The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023)

	Ref	Expression
Hypotheses	rrxsca.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
	rrx0.0	⊢ 0 = ( 𝐼 × { 0 } )
Assertion	rrx0	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝐻 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		rrxsca.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2		rrx0.0	⊢ 0 = ( 𝐼 × { 0 } )
3	1	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4	3	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝐻 ) = ( 0g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
5		eqid	⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
6		eqid	⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
7		eqid	⊢ ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) )
8	5 6 7	tcphval	⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) )
9	8	a1i	⊢ ( 𝐼 ∈ 𝑉 → ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) )
10	9	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( 0g ‘ ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
11		fvexd	⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∈ V )
12	11	mptexd	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ∈ V )
13		eqid	⊢ ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) = ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) )
14		eqid	⊢ ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) )
15	13 14	tng0	⊢ ( ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ∈ V → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 0g ‘ ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
16	12 15	syl	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 0g ‘ ( ( ℝfld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
17		refld	⊢ ℝfld ∈ Field
18		isfld	⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
19		drngring	⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
20	19	adantr	⊢ ( ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) → ℝfld ∈ Ring )
21	18 20	sylbi	⊢ ( ℝfld ∈ Field → ℝfld ∈ Ring )
22	17 21	ax-mp	⊢ ℝfld ∈ Ring
23		eqid	⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
24		re0g	⊢ 0 = ( 0g ‘ ℝfld )
25	23 24	frlm0	⊢ ( ( ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) )
26	22 25	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) )
27	2 26	syl5req	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = 0 )
28	10 16 27	3eqtr2d	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = 0 )
29	4 28	eqtrd	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝐻 ) = 0 )