Metamath Proof Explorer

Theorem rrxmetlem

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

Ref Expression
Hypotheses rrxmval.1 
|- X = { h e. ( RR ^m I ) | h finSupp 0 }
rrxmval.d 
|- D = ( dist ` ( RR^ ` I ) )
rrxmetlem.1 
|- ( ph -> I e. V )
rrxmetlem.2 
|- ( ph -> F e. X )
rrxmetlem.3 
|- ( ph -> G e. X )
rrxmetlem.4 
|- ( ph -> A C_ I )
rrxmetlem.5 
|- ( ph -> A e. Fin )
rrxmetlem.6 
|- ( ph -> ( ( F supp 0 ) u. ( G supp 0 ) ) C_ A )
Assertion rrxmetlem 
|- ( ph -> sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. A ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 
 |-  X = { h e. ( RR ^m I ) | h finSupp 0 }
2 rrxmval.d 
 |-  D = ( dist ` ( RR^ ` I ) )
3 rrxmetlem.1 
 |-  ( ph -> I e. V )
4 rrxmetlem.2 
 |-  ( ph -> F e. X )
5 rrxmetlem.3 
 |-  ( ph -> G e. X )
6 rrxmetlem.4 
 |-  ( ph -> A C_ I )
7 rrxmetlem.5 
 |-  ( ph -> A e. Fin )
8 rrxmetlem.6 
 |-  ( ph -> ( ( F supp 0 ) u. ( G supp 0 ) ) C_ A )
9 8 6 sstrd 
 |-  ( ph -> ( ( F supp 0 ) u. ( G supp 0 ) ) C_ I )
10 9 sselda 
 |-  ( ( ph /\ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ) -> k e. I )
11 1 4 rrxf 
 |-  ( ph -> F : I --> RR )
12 11 ffvelcdmda 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. RR )
13 12 recnd 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. CC )
14 10 13 syldan 
 |-  ( ( ph /\ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ) -> ( F ` k ) e. CC )
15 1 5 rrxf 
 |-  ( ph -> G : I --> RR )
16 15 ffvelcdmda 
 |-  ( ( ph /\ k e. I ) -> ( G ` k ) e. RR )
17 16 recnd 
 |-  ( ( ph /\ k e. I ) -> ( G ` k ) e. CC )
18 10 17 syldan 
 |-  ( ( ph /\ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ) -> ( G ` k ) e. CC )
19 14 18 subcld 
 |-  ( ( ph /\ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ) -> ( ( F ` k ) - ( G ` k ) ) e. CC )
20 19 sqcld 
 |-  ( ( ph /\ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. CC )
21 6 ssdifd 
 |-  ( ph -> ( A \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) C_ ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) )
22 21 sselda 
 |-  ( ( ph /\ k e. ( A \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) )
23 simpr 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) )
24 23 eldifad 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> k e. I )
25 24 13 syldan 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( F ` k ) e. CC )
26 ssun1 
 |-  ( F supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) )
27 26 a1i 
 |-  ( ph -> ( F supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
28 0red 
 |-  ( ph -> 0 e. RR )
29 11 27 3 28 suppssr 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( F ` k ) = 0 )
30 ssun2 
 |-  ( G supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) )
31 30 a1i 
 |-  ( ph -> ( G supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
32 15 31 3 28 suppssr 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( G ` k ) = 0 )
33 29 32 eqtr4d 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( F ` k ) = ( G ` k ) )
34 25 33 subeq0bd 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( ( F ` k ) - ( G ` k ) ) = 0 )
35 34 sq0id 
 |-  ( ( ph /\ k e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = 0 )
36 22 35 syldan 
 |-  ( ( ph /\ k e. ( A \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = 0 )
37 8 20 36 7 fsumss 
 |-  ( ph -> sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. A ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )