Metamath Proof Explorer

Theorem rrxnm

Description: The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxnm ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) ) ) = ( norm ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 resrng ⊢ ℝfld ∈ *-Ring
4 srngring ⊢ ( ℝfld ∈ *-Ring → ℝfld ∈ Ring )
5 3 4 ax-mp ⊢ ℝfld ∈ Ring
6 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
7 6 frlmlmod ⊢ ( ( ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld freeLMod 𝐼 ) ∈ LMod )
8 5 7 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld freeLMod 𝐼 ) ∈ LMod )
9 lmodgrp ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ LMod → ( ℝfld freeLMod 𝐼 ) ∈ Grp )
10 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
11 eqid ⊢ ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
12 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
13 eqid ⊢ ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) )
14 10 11 12 13 tchnmfval ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ Grp → ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) ) ) )
15 8 9 14 3syl ⊢ ( 𝐼 ∈ 𝑉 → ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) ) ) )
16 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
17 16 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( norm ‘ 𝐻 ) = ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
18 16 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
19 10 12 tcphbas ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
20 18 2 19 3eqtr4g ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
21 1 2 rrxbase ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } )
22 ssrab2 ⊢ { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } ⊆ ( ℝ ↑m 𝐼 )
23 21 22 eqsstrdi ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 ⊆ ( ℝ ↑m 𝐼 ) )
24 23 sselda ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
25 16 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( ·𝑖 ‘ 𝐻 ) = ( ·𝑖 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
26 1 2 rrxip ⊢ ( 𝐼 ∈ 𝑉 → ( ℎ ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝐻 ) )
27 10 13 tcphip ⊢ ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑖 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
28 27 a1i ⊢ ( 𝐼 ∈ 𝑉 → ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑖 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
29 25 26 28 3eqtr4rd ⊢ ( 𝐼 ∈ 𝑉 → ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ℎ ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
30 29 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) → ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ℎ ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
31 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ℎ = 𝑓 )
32 31 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ( ℎ ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
33 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → 𝑔 = 𝑓 )
34 33 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
35 32 34 oveq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
36 35 adantr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
37 elmapi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℝ )
38 37 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑓 : 𝐼 ⟶ ℝ )
39 38 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
40 39 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
41 40 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
42 41 sqvald ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
43 36 42 eqtr4d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) )
44 43 mpteq2dva ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) )
45 44 oveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) ∧ ( ℎ = 𝑓 ∧ 𝑔 = 𝑓 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) )
46 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
47 ovexd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) ∈ V )
48 30 45 46 46 47 ovmpod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) )
49 24 48 syldan ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) )
50 49 eqcomd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) = ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) )
51 50 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) ) = ( √ ‘ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) ) )
52 20 51 mpteq12dva ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) ) ) )
53 15 17 52 3eqtr4rd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ↑ 2 ) ) ) ) ) = ( norm ‘ 𝐻 ) )