Metamath Proof Explorer

Theorem angmgmaddov1lem

Description: Lemma for angmgmaddov1 . (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p 
|- P = ( Base ` G )
angmgmadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmadd.i 
|- I = ( Itv ` G )
angmgmadd.d 
|- .- = ( dist ` G )
angmgmadd.c 
|- .~ = ( cgrA ` G )
angmgmadd.l 
|- L = ( LineG ` G )
angmgmadd.g 
|- ( ph -> G e. TarskiG )
angmgmaddov.u 
|- ( ph -> U e. P )
angmgmaddov.v 
|- ( ph -> V e. P )
angmgmaddov.w 
|- ( ph -> W e. P )
angmgmaddov.x 
|- ( ph -> X e. P )
angmgmaddov.y 
|- ( ph -> Y e. P )
angmgmaddov.z 
|- ( ph -> Z e. P )
angmgmaddeu.1 
|- ( ph -> U =/= V )
angmgmaddeu.2 
|- ( ph -> V =/= W )
angmgmaddeu.3 
|- ( ph -> X =/= Y )
angmgmaddeu.4 
|- ( ph -> Y =/= Z )
angmgmaddov1lem.1 
|- ( ph -> -. X e. ( Y L Z ) )
Assertion angmgmaddov1lem 
|- ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 angmgmadd.p 
 |-  P = ( Base ` G )
2 angmgmadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmadd.i 
 |-  I = ( Itv ` G )
4 angmgmadd.d 
 |-  .- = ( dist ` G )
5 angmgmadd.c 
 |-  .~ = ( cgrA ` G )
6 angmgmadd.l 
 |-  L = ( LineG ` G )
7 angmgmadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmgmaddov.u 
 |-  ( ph -> U e. P )
9 angmgmaddov.v 
 |-  ( ph -> V e. P )
10 angmgmaddov.w 
 |-  ( ph -> W e. P )
11 angmgmaddov.x 
 |-  ( ph -> X e. P )
12 angmgmaddov.y 
 |-  ( ph -> Y e. P )
13 angmgmaddov.z 
 |-  ( ph -> Z e. P )
14 angmgmaddeu.1 
 |-  ( ph -> U =/= V )
15 angmgmaddeu.2 
 |-  ( ph -> V =/= W )
16 angmgmaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmgmaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmgmaddov1lem.1 
 |-  ( ph -> -. X e. ( Y L Z ) )
19 7 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> G e. TarskiG )
20 8 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> U e. P )
21 9 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> V e. P )
22 10 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> W e. P )
23 11 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> X e. P )
24 12 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> Y e. P )
25 13 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> Z e. P )
26 14 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> U =/= V )
27 15 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> V =/= W )
28 16 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> X =/= Y )
29 17 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> Y =/= Z )
30 18 adantr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> -. X e. ( Y L Z ) )
31 simpr 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> U ( ( hlG ` G ) ` V ) W )
32 1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31 angmgmaddeu2 
 |-  ( ( ph /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
33 32 adantlr 
 |-  ( ( ( ph /\ U e. ( V L W ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
34 7 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> G e. TarskiG )
35 8 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> U e. P )
36 9 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> V e. P )
37 10 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> W e. P )
38 11 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> X e. P )
39 12 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> Y e. P )
40 13 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> Z e. P )
41 14 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> U =/= V )
42 15 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> V =/= W )
43 16 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> X =/= Y )
44 17 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> Y =/= Z )
45 18 adantr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> -. X e. ( Y L Z ) )
46 simpr 
 |-  ( ( ph /\ V e. ( W I U ) ) -> V e. ( W I U ) )
47 1 4 3 34 37 36 35 46 tgbtwncom 
 |-  ( ( ph /\ V e. ( W I U ) ) -> V e. ( U I W ) )
48 1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 45 47 angmgmaddeu3 
 |-  ( ( ph /\ V e. ( W I U ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
49 48 adantlr 
 |-  ( ( ( ph /\ U e. ( V L W ) ) /\ V e. ( W I U ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
50 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
51 10 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> W e. P )
52 9 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> V e. P )
53 8 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> U e. P )
54 7 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> G e. TarskiG )
55 11 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> X e. P )
56 15 necomd 
 |-  ( ph -> W =/= V )
57 56 adantr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> W =/= V )
58 simpr 
 |-  ( ( ph /\ U e. ( V L W ) ) -> U e. ( V L W ) )
59 1 3 6 54 51 52 53 57 58 lncom 
 |-  ( ( ph /\ U e. ( V L W ) ) -> U e. ( W L V ) )
60 1 3 50 51 52 53 54 55 6 59 lnhl 
 |-  ( ( ph /\ U e. ( V L W ) ) -> ( U ( ( hlG ` G ) ` V ) W \/ V e. ( W I U ) ) )
61 33 49 60 mpjaodan 
 |-  ( ( ph /\ U e. ( V L W ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
62 7 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> G e. TarskiG )
63 8 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> U e. P )
64 9 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> V e. P )
65 10 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> W e. P )
66 11 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> X e. P )
67 12 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> Y e. P )
68 13 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> Z e. P )
69 14 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> U =/= V )
70 15 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> V =/= W )
71 16 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> X =/= Y )
72 17 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> Y =/= Z )
73 18 adantr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> -. X e. ( Y L Z ) )
74 simpr 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> -. U e. ( V L W ) )
75 1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74 angmgmaddeu1 
 |-  ( ( ph /\ -. U e. ( V L W ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
76 61 75 pm2.61dan 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )