Metamath Proof Explorer

Theorem eenglngeehlnm

Description: The line definition in the Tarski structure for the Euclidean geometry (see elntg ) corresponds to the definition of lines passing through two different points in a left module (see rrxlines ). (Contributed by AV, 16-Feb-2023)

Ref Expression
Assertion eenglngeehlnm 
|- ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( LineM ` ( EEhil ` N ) ) )

Proof

Step Hyp Ref Expression
1 eengbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
2 1 eqcomd 
 |-  ( N e. NN -> ( Base ` ( EEG ` N ) ) = ( EE ` N ) )
3 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
4 3 oveq2d 
 |-  ( n = N -> ( RR ^m ( 1 ... n ) ) = ( RR ^m ( 1 ... N ) ) )
5 df-ee 
 |-  EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
6 ovex 
 |-  ( RR ^m ( 1 ... N ) ) e. _V
7 4 5 6 fvmpt 
 |-  ( N e. NN -> ( EE ` N ) = ( RR ^m ( 1 ... N ) ) )
8 2 7 eqtrd 
 |-  ( N e. NN -> ( Base ` ( EEG ` N ) ) = ( RR ^m ( 1 ... N ) ) )
9 2 ancli 
 |-  ( N e. NN -> ( N e. NN /\ ( Base ` ( EEG ` N ) ) = ( EE ` N ) ) )
10 9 8 jca 
 |-  ( N e. NN -> ( ( N e. NN /\ ( Base ` ( EEG ` N ) ) = ( EE ` N ) ) /\ ( Base ` ( EEG ` N ) ) = ( RR ^m ( 1 ... N ) ) ) )
11 difeq1 
 |-  ( ( Base ` ( EEG ` N ) ) = ( RR ^m ( 1 ... N ) ) -> ( ( Base ` ( EEG ` N ) ) \ { x } ) = ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
12 11 ad2antlr 
 |-  ( ( ( ( N e. NN /\ ( Base ` ( EEG ` N ) ) = ( EE ` N ) ) /\ ( Base ` ( EEG ` N ) ) = ( RR ^m ( 1 ... N ) ) ) /\ x e. ( Base ` ( EEG ` N ) ) ) -> ( ( Base ` ( EEG ` N ) ) \ { x } ) = ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
13 10 12 sylan 
 |-  ( ( N e. NN /\ x e. ( Base ` ( EEG ` N ) ) ) -> ( ( Base ` ( EEG ` N ) ) \ { x } ) = ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
14 8 adantr 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) -> ( Base ` ( EEG ` N ) ) = ( RR ^m ( 1 ... N ) ) )
15 simpll 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) /\ p e. ( Base ` ( EEG ` N ) ) ) -> N e. NN )
16 8 eleq2d 
 |-  ( N e. NN -> ( x e. ( Base ` ( EEG ` N ) ) <-> x e. ( RR ^m ( 1 ... N ) ) ) )
17 16 biimpcd 
 |-  ( x e. ( Base ` ( EEG ` N ) ) -> ( N e. NN -> x e. ( RR ^m ( 1 ... N ) ) ) )
18 17 adantr 
 |-  ( ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) -> ( N e. NN -> x e. ( RR ^m ( 1 ... N ) ) ) )
19 18 impcom 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) -> x e. ( RR ^m ( 1 ... N ) ) )
20 19 adantr 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) /\ p e. ( Base ` ( EEG ` N ) ) ) -> x e. ( RR ^m ( 1 ... N ) ) )
21 8 difeq1d 
 |-  ( N e. NN -> ( ( Base ` ( EEG ` N ) ) \ { x } ) = ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
22 21 eleq2d 
 |-  ( N e. NN -> ( y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) <-> y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) )
23 22 biimpd 
 |-  ( N e. NN -> ( y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) -> y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) )
24 23 adantld 
 |-  ( N e. NN -> ( ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) -> y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) )
25 24 imp 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) -> y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
26 25 adantr 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) /\ p e. ( Base ` ( EEG ` N ) ) ) -> y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) )
27 14 eleq2d 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) -> ( p e. ( Base ` ( EEG ` N ) ) <-> p e. ( RR ^m ( 1 ... N ) ) ) )
28 27 biimpa 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) /\ p e. ( Base ` ( EEG ` N ) ) ) -> p e. ( RR ^m ( 1 ... N ) ) )
29 eenglngeehlnmlem1 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
30 eenglngeehlnmlem2 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) ) )
31 29 30 impbid 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) <-> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
32 15 20 26 28 31 syl31anc 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) /\ p e. ( Base ` ( EEG ` N ) ) ) -> ( ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) <-> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
33 14 32 rabeqbidva 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) ) ) -> { p e. ( Base ` ( EEG ` N ) ) | ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) } = { p e. ( RR ^m ( 1 ... N ) ) | E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } )
34 8 13 33 mpoeq123dva 
 |-  ( N e. NN -> ( x e. ( Base ` ( EEG ` N ) ) , y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) |-> { p e. ( Base ` ( EEG ` N ) ) | ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) } ) = ( x e. ( RR ^m ( 1 ... N ) ) , y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) |-> { p e. ( RR ^m ( 1 ... N ) ) | E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )
35 eqid 
 |-  ( Base ` ( EEG ` N ) ) = ( Base ` ( EEG ` N ) )
36 eqid 
 |-  ( 1 ... N ) = ( 1 ... N )
37 35 36 elntg2 
 |-  ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( x e. ( Base ` ( EEG ` N ) ) , y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) |-> { p e. ( Base ` ( EEG ` N ) ) | ( E. z e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - z ) x. ( x ` i ) ) + ( z x. ( y ` i ) ) ) \/ E. v e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - v ) x. ( p ` i ) ) + ( v x. ( y ` i ) ) ) \/ E. w e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - w ) x. ( x ` i ) ) + ( w x. ( p ` i ) ) ) ) } ) )
38 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
39 eqid 
 |-  ( EEhil ` N ) = ( EEhil ` N )
40 39 ehlval 
 |-  ( N e. NN0 -> ( EEhil ` N ) = ( RR^ ` ( 1 ... N ) ) )
41 38 40 syl 
 |-  ( N e. NN -> ( EEhil ` N ) = ( RR^ ` ( 1 ... N ) ) )
42 41 fveq2d 
 |-  ( N e. NN -> ( LineM ` ( EEhil ` N ) ) = ( LineM ` ( RR^ ` ( 1 ... N ) ) ) )
43 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
44 eqid 
 |-  ( RR^ ` ( 1 ... N ) ) = ( RR^ ` ( 1 ... N ) )
45 eqid 
 |-  ( RR ^m ( 1 ... N ) ) = ( RR ^m ( 1 ... N ) )
46 eqid 
 |-  ( LineM ` ( RR^ ` ( 1 ... N ) ) ) = ( LineM ` ( RR^ ` ( 1 ... N ) ) )
47 44 45 46 rrxlinesc 
 |-  ( ( 1 ... N ) e. Fin -> ( LineM ` ( RR^ ` ( 1 ... N ) ) ) = ( x e. ( RR ^m ( 1 ... N ) ) , y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) |-> { p e. ( RR ^m ( 1 ... N ) ) | E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )
48 43 47 syl 
 |-  ( N e. NN -> ( LineM ` ( RR^ ` ( 1 ... N ) ) ) = ( x e. ( RR ^m ( 1 ... N ) ) , y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) |-> { p e. ( RR ^m ( 1 ... N ) ) | E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )
49 42 48 eqtrd 
 |-  ( N e. NN -> ( LineM ` ( EEhil ` N ) ) = ( x e. ( RR ^m ( 1 ... N ) ) , y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) |-> { p e. ( RR ^m ( 1 ... N ) ) | E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )
50 34 37 49 3eqtr4d 
 |-  ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( LineM ` ( EEhil ` N ) ) )