Metamath Proof Explorer

Theorem rrxmetlem

Description: Lemma for rrxmet . (Contributed by Thierry Arnoux, 5-Jul-2019)

Ref Expression
Hypotheses rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
rrxmetlem.1 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
rrxmetlem.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
rrxmetlem.3 ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
rrxmetlem.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )
rrxmetlem.5 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
rrxmetlem.6 ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐴 )
Assertion rrxmetlem ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 rrxmetlem.1 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 rrxmetlem.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
5 rrxmetlem.3 ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
6 rrxmetlem.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )
7 rrxmetlem.5 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
8 rrxmetlem.6 ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐴 )
9 8 6 sstrd ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐼 )
10 9 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → 𝑘 ∈ 𝐼 )
11 1 4 rrxf ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14 10 13 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
15 1 5 rrxf ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ ℝ )
16 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
17 16 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
18 10 17 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
19 14 18 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
20 19 sqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℂ )
21 6 ssdifd ⊢ ( 𝜑 → ( 𝐴 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ⊆ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) )
22 21 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) )
24 23 eldifad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → 𝑘 ∈ 𝐼 )
25 24 13 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
26 ssun1 ⊢ ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
27 26 a1i ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
28 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
29 11 27 3 28 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = 0 )
30 ssun2 ⊢ ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
31 30 a1i ⊢ ( 𝜑 → ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
32 15 31 3 28 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 ‘ 𝑘 ) = 0 )
33 29 32 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
34 25 33 subeq0bd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) = 0 )
35 34 sq0id ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = 0 )
36 22 35 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = 0 )
37 8 20 36 7 fsumss ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )