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 
|- X = { h e. ( RR ^m I ) | h finSupp 0 }
Assertion rrxmvallem 
|- ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 
 |-  X = { h e. ( RR ^m I ) | h finSupp 0 }
2 simprl 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( F ` x ) = 0 )
3 0cn 
 |-  0 e. CC
4 2 3 eqeltrdi 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( F ` x ) e. CC )
5 simprr 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( G ` x ) = 0 )
6 2 5 eqtr4d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( F ` x ) = ( G ` x ) )
7 4 6 subeq0bd 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( ( F ` x ) - ( G ` x ) ) = 0 )
8 7 sq0id 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) -> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) = 0 )
9 8 ex 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) -> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) = 0 ) )
10 ioran 
 |-  ( -. ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) <-> ( -. ( F ` x ) =/= 0 /\ -. ( G ` x ) =/= 0 ) )
11 nne 
 |-  ( -. ( F ` x ) =/= 0 <-> ( F ` x ) = 0 )
12 nne 
 |-  ( -. ( G ` x ) =/= 0 <-> ( G ` x ) = 0 )
13 11 12 anbi12i 
 |-  ( ( -. ( F ` x ) =/= 0 /\ -. ( G ` x ) =/= 0 ) <-> ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) )
14 10 13 bitri 
 |-  ( -. ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) <-> ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) )
15 14 a1i 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( -. ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) <-> ( ( F ` x ) = 0 /\ ( G ` x ) = 0 ) ) )
16 eqidd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) = ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
17 simpr 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ k = x ) -> k = x )
18 17 fveq2d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ k = x ) -> ( F ` k ) = ( F ` x ) )
19 17 fveq2d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ k = x ) -> ( G ` k ) = ( G ` x ) )
20 18 19 oveq12d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ k = x ) -> ( ( F ` k ) - ( G ` k ) ) = ( ( F ` x ) - ( G ` x ) ) )
21 20 oveq1d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) /\ k = x ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
22 simpr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> x e. I )
23 ovex 
 |-  ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) e. _V
24 23 a1i 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) e. _V )
25 16 21 22 24 fvmptd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) = ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
26 25 neeq1d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 <-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) =/= 0 ) )
27 26 bicomd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) =/= 0 <-> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 ) )
28 27 necon1bbid 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( -. ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 <-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) = 0 ) )
29 9 15 28 3imtr4d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( -. ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) -> -. ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 ) )
30 29 con4d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 -> ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) ) )
31 30 ss2rabdv 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> { x e. I | ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 } C_ { x e. I | ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) } )
32 unrab 
 |-  ( { x e. I | ( F ` x ) =/= 0 } u. { x e. I | ( G ` x ) =/= 0 } ) = { x e. I | ( ( F ` x ) =/= 0 \/ ( G ` x ) =/= 0 ) }
33 31 32 sseqtrrdi 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> { x e. I | ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 } C_ ( { x e. I | ( F ` x ) =/= 0 } u. { x e. I | ( G ` x ) =/= 0 } ) )
34 simp1 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> I e. V )
35 ovex 
 |-  ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. _V
36 eqid 
 |-  ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) = ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
37 35 36 fnmpti 
 |-  ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) Fn I
38 suppvalfn 
 |-  ( ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) Fn I /\ I e. V /\ 0 e. CC ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) = { x e. I | ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 } )
39 37 3 38 mp3an13 
 |-  ( I e. V -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) = { x e. I | ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 } )
40 34 39 syl 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) = { x e. I | ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ` x ) =/= 0 } )
41 elrabi 
 |-  ( F e. { h e. ( RR ^m I ) | h finSupp 0 } -> F e. ( RR ^m I ) )
42 41 1 eleq2s 
 |-  ( F e. X -> F e. ( RR ^m I ) )
43 elmapi 
 |-  ( F e. ( RR ^m I ) -> F : I --> RR )
44 ffn 
 |-  ( F : I --> RR -> F Fn I )
45 42 43 44 3syl 
 |-  ( F e. X -> F Fn I )
46 45 3ad2ant2 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> F Fn I )
47 3 a1i 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> 0 e. CC )
48 suppvalfn 
 |-  ( ( F Fn I /\ I e. V /\ 0 e. CC ) -> ( F supp 0 ) = { x e. I | ( F ` x ) =/= 0 } )
49 46 34 47 48 syl3anc 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( F supp 0 ) = { x e. I | ( F ` x ) =/= 0 } )
50 elrabi 
 |-  ( G e. { h e. ( RR ^m I ) | h finSupp 0 } -> G e. ( RR ^m I ) )
51 50 1 eleq2s 
 |-  ( G e. X -> G e. ( RR ^m I ) )
52 elmapi 
 |-  ( G e. ( RR ^m I ) -> G : I --> RR )
53 ffn 
 |-  ( G : I --> RR -> G Fn I )
54 51 52 53 3syl 
 |-  ( G e. X -> G Fn I )
55 54 3ad2ant3 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> G Fn I )
56 suppvalfn 
 |-  ( ( G Fn I /\ I e. V /\ 0 e. CC ) -> ( G supp 0 ) = { x e. I | ( G ` x ) =/= 0 } )
57 55 34 47 56 syl3anc 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( G supp 0 ) = { x e. I | ( G ` x ) =/= 0 } )
58 49 57 uneq12d 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) = ( { x e. I | ( F ` x ) =/= 0 } u. { x e. I | ( G ` x ) =/= 0 } ) )
59 33 40 58 3sstr4d 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )