Metamath Proof Explorer

Theorem eengv

Description: The value of the Euclidean geometry for dimension N . (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengv 
|- ( N e. NN -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
2 1 opeq2d 
 |-  ( n = N -> <. ( Base ` ndx ) , ( EE ` n ) >. = <. ( Base ` ndx ) , ( EE ` N ) >. )
3 1 adantr 
 |-  ( ( n = N /\ x e. ( EE ` n ) ) -> ( EE ` n ) = ( EE ` N ) )
4 simpl 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( EE ` n ) ) ) -> n = N )
5 4 oveq2d 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( EE ` n ) ) ) -> ( 1 ... n ) = ( 1 ... N ) )
6 5 sumeq1d 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( EE ` n ) ) ) -> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) )
7 1 3 6 mpoeq123dva 
 |-  ( n = N -> ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) = ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) )
8 7 opeq2d 
 |-  ( n = N -> <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. = <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. )
9 2 8 preq12d 
 |-  ( n = N -> { <. ( Base ` ndx ) , ( EE ` n ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } = { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } )
10 1 adantr 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( EE ` n ) ) ) -> ( EE ` n ) = ( EE ` N ) )
11 10 rabeqdv 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( EE ` n ) ) ) -> { z e. ( EE ` n ) | z Btwn <. x , y >. } = { z e. ( EE ` N ) | z Btwn <. x , y >. } )
12 1 3 11 mpoeq123dva 
 |-  ( n = N -> ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) = ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) )
13 12 opeq2d 
 |-  ( n = N -> <. ( Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >. = <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. )
14 3 difeq1d 
 |-  ( ( n = N /\ x e. ( EE ` n ) ) -> ( ( EE ` n ) \ { x } ) = ( ( EE ` N ) \ { x } ) )
15 1 rabeqdv 
 |-  ( n = N -> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } = { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } )
16 15 adantr 
 |-  ( ( n = N /\ ( x e. ( EE ` n ) /\ y e. ( ( EE ` n ) \ { x } ) ) ) -> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } = { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } )
17 1 14 16 mpoeq123dva 
 |-  ( n = N -> ( x e. ( EE ` n ) , y e. ( ( EE ` n ) \ { x } ) |-> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) = ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) )
18 17 opeq2d 
 |-  ( n = N -> <. ( LineG ` ndx ) , ( x e. ( EE ` n ) , y e. ( ( EE ` n ) \ { x } ) |-> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. = <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. )
19 13 18 preq12d 
 |-  ( n = N -> { <. ( Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` n ) , y e. ( ( EE ` n ) \ { x } ) |-> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } = { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } )
20 9 19 uneq12d 
 |-  ( n = N -> ( { <. ( Base ` ndx ) , ( EE ` n ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` n ) , y e. ( ( EE ` n ) \ { x } ) |-> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
21 df-eeng 
 |-  EEG = ( n e. NN |-> ( { <. ( Base ` ndx ) , ( EE ` n ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` n ) , y e. ( ( EE ` n ) \ { x } ) |-> { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
22 prex 
 |-  { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } e. _V
23 prex 
 |-  { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } e. _V
24 22 23 unex 
 |-  ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) e. _V
25 20 21 24 fvmpt 
 |-  ( N e. NN -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )