Metamath Proof Explorer

Theorem rrxmvallem

Description: Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypothesis rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
Assertion rrxmvallem ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 simprl ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
3 0cn ⊢ 0 ∈ ℂ
4 2 3 eqeltrdi ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
5 simprr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 ‘ 𝑥 ) = 0 )
6 2 5 eqtr4d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
7 4 6 subeq0bd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = 0 )
8 7 sq0id ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) = 0 )
9 8 ex ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) = 0 ) )
10 ioran ⊢ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ↔ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ¬ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
11 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
12 nne ⊢ ( ¬ ( 𝐺 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐺 ‘ 𝑥 ) = 0 )
13 11 12 anbi12i ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 0 ∧ ¬ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) )
14 10 13 bitri ⊢ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) )
15 14 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ¬ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
16 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
17 simpr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 = 𝑥 ) → 𝑘 = 𝑥 )
18 17 fveq2d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 = 𝑥 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
19 17 fveq2d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 = 𝑥 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑥 ) )
20 18 19 oveq12d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 = 𝑥 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
21 20 oveq1d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 = 𝑥 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
22 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
23 ovex ⊢ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ∈ V
24 23 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ∈ V )
25 16 21 22 24 fvmptd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
26 25 neeq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 ↔ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ≠ 0 ) )
27 26 bicomd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ≠ 0 ↔ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 ) )
28 27 necon1bbid ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ¬ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 ↔ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) = 0 ) )
29 9 15 28 3imtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ¬ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) → ¬ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 ) )
30 29 con4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 → ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ) )
31 30 ss2rabdv ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 } ⊆ { 𝑥 ∈ 𝐼 ∣ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) } )
32 unrab ⊢ ( { 𝑥 ∈ 𝐼 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 0 } ∪ { 𝑥 ∈ 𝐼 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝐹 ‘ 𝑥 ) ≠ 0 ∨ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) }
33 31 32 sseqtrrdi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 } ⊆ ( { 𝑥 ∈ 𝐼 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 0 } ∪ { 𝑥 ∈ 𝐼 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } ) )
34 simp1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
35 ovex ⊢ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ V
36 eqid ⊢ ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
37 35 36 fnmpti ⊢ ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) Fn 𝐼
38 suppvalfn ⊢ ( ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 } )
39 37 3 38 mp3an13 ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 } )
40 34 39 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ‘ 𝑥 ) ≠ 0 } )
41 elrabi ⊢ ( 𝐹 ∈ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
42 41 1 eleq2s ⊢ ( 𝐹 ∈ 𝑋 → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
43 elmapi ⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
44 ffn ⊢ ( 𝐹 : 𝐼 ⟶ ℝ → 𝐹 Fn 𝐼 )
45 42 43 44 3syl ⊢ ( 𝐹 ∈ 𝑋 → 𝐹 Fn 𝐼 )
46 45 3ad2ant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 Fn 𝐼 )
47 3 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 0 ∈ ℂ )
48 suppvalfn ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ ℂ ) → ( 𝐹 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 0 } )
49 46 34 47 48 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 0 } )
50 elrabi ⊢ ( 𝐺 ∈ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
51 50 1 eleq2s ⊢ ( 𝐺 ∈ 𝑋 → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
52 elmapi ⊢ ( 𝐺 ∈ ( ℝ ↑m 𝐼 ) → 𝐺 : 𝐼 ⟶ ℝ )
53 ffn ⊢ ( 𝐺 : 𝐼 ⟶ ℝ → 𝐺 Fn 𝐼 )
54 51 52 53 3syl ⊢ ( 𝐺 ∈ 𝑋 → 𝐺 Fn 𝐼 )
55 54 3ad2ant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 Fn 𝐼 )
56 suppvalfn ⊢ ( ( 𝐺 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ ℂ ) → ( 𝐺 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } )
57 55 34 47 56 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐺 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } )
58 49 57 uneq12d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) = ( { 𝑥 ∈ 𝐼 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 0 } ∪ { 𝑥 ∈ 𝐼 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } ) )
59 33 40 58 3sstr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )