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

Metamath Proof Explorer

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 eqtr2id ⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = 0 )
28 10 16 27 3eqtr2d ⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = 0 )
29 4 28 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝐻 ) = 0 )