Metamath Proof Explorer

Theorem angmgmaddcl

Description: Closure of the addition of angles. (Contributed by Thierry Arnoux, 31-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 )
angmgmadd.o 
|- .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
angmgmaddcl.1 
|- ( ph -> E e. A )
angmgmaddcl.2 
|- ( ph -> F e. A )
Assertion angmgmaddcl 
|- ( ph -> ( E .+ F ) e. A )

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 angmgmadd.o 
 |-  .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
9 angmgmaddcl.1 
 |-  ( ph -> E e. A )
10 angmgmaddcl.2 
 |-  ( ph -> F e. A )
11 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) -> E = <" x y z "> )
12 11 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) -> E = <" x y z "> )
13 12 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> E = <" x y z "> )
14 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> F = <" u v w "> )
15 13 14 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( E .+ F ) = ( <" x y z "> .+ <" u v w "> ) )
16 7 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ y e. P ) -> G e. TarskiG )
17 16 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> G e. TarskiG )
18 17 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> G e. TarskiG )
19 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> u e. P )
20 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> v e. P )
21 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> w e. P )
22 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ y e. P ) -> x e. P )
23 22 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> x e. P )
24 23 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> x e. P )
25 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> y e. P )
26 25 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> y e. P )
27 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) -> z e. P )
28 27 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> z e. P )
29 28 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> z e. P )
30 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> u =/= v )
31 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> v =/= w )
32 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> x =/= y )
33 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> y =/= z )
34 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> x e. ( y L z ) )
35 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> t e. P )
36 simprl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> <" w v t "> .~ <" x y z "> )
37 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( v .- t ) = ( y .- x ) )
38 1 2 3 4 5 6 18 19 20 21 24 26 29 30 31 32 33 8 34 35 36 37 angmgmaddov2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( <" x y z "> .+ <" u v w "> ) = <" u v t "> )
39 15 38 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( E .+ F ) = <" u v t "> )
40 1 fvexi 
 |-  P e. _V
41 40 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> P e. _V )
42 37 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( y .- x ) = ( v .- t ) )
43 32 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> y =/= x )
44 1 4 3 18 26 24 20 35 42 43 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> v =/= t )
45 2 41 19 20 35 30 44 elcgrabasrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> <" u v t "> e. A )
46 39 45 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) /\ t e. P ) /\ ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) -> ( E .+ F ) e. A )
47 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) -> G e. TarskiG )
48 47 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> G e. TarskiG )
49 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> u e. P )
50 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> v e. P )
51 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> w e. P )
52 22 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) -> x e. P )
53 52 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> x e. P )
54 25 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> y e. P )
55 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> z e. P )
56 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> u =/= v )
57 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> v =/= w )
58 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> x =/= y )
59 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> y =/= z )
60 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> x e. ( y L z ) )
61 1 2 3 4 5 6 48 49 50 51 53 54 55 56 57 58 59 60 angmgmaddov2lem 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> E! s e. P ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) )
62 reurex 
 |-  ( E! s e. P ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) -> E. s e. P ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) )
63 61 62 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> E. s e. P ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) )
64 eqidd 
 |-  ( s = t -> w = w )
65 eqidd 
 |-  ( s = t -> v = v )
66 id 
 |-  ( s = t -> s = t )
67 64 65 66 s3eqd 
 |-  ( s = t -> <" w v s "> = <" w v t "> )
68 67 breq1d 
 |-  ( s = t -> ( <" w v s "> .~ <" x y z "> <-> <" w v t "> .~ <" x y z "> ) )
69 oveq2 
 |-  ( s = t -> ( v .- s ) = ( v .- t ) )
70 69 eqeq1d 
 |-  ( s = t -> ( ( v .- s ) = ( y .- x ) <-> ( v .- t ) = ( y .- x ) ) )
71 68 70 anbi12d 
 |-  ( s = t -> ( ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) <-> ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) ) )
72 71 cbvrexvw 
 |-  ( E. s e. P ( <" w v s "> .~ <" x y z "> /\ ( v .- s ) = ( y .- x ) ) <-> E. t e. P ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) )
73 63 72 sylib 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> E. t e. P ( <" w v t "> .~ <" x y z "> /\ ( v .- t ) = ( y .- x ) ) )
74 46 73 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ x e. ( y L z ) ) -> ( E .+ F ) e. A )
75 11 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> E = <" x y z "> )
76 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> F = <" u v w "> )
77 75 76 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( E .+ F ) = ( <" x y z "> .+ <" u v w "> ) )
78 17 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> G e. TarskiG )
79 78 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> G e. TarskiG )
80 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> u e. P )
81 80 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> u e. P )
82 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> v e. P )
83 82 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> v e. P )
84 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> w e. P )
85 84 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> w e. P )
86 23 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> x e. P )
87 86 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> x e. P )
88 25 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> y e. P )
89 88 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> y e. P )
90 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> z e. P )
91 90 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> z e. P )
92 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> u =/= v )
93 92 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> u =/= v )
94 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> v =/= w )
95 94 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> v =/= w )
96 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> x =/= y )
97 96 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> x =/= y )
98 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> y =/= z )
99 98 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> y =/= z )
100 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> -. x e. ( y L z ) )
101 100 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> -. x e. ( y L z ) )
102 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> t e. P )
103 simpr1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> <" z y t "> .~ <" u v w "> )
104 simpr2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( y .- t ) = ( v .- u ) )
105 simpr3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( ( y L z ) i^i ( t I x ) ) =/= (/) )
106 1 2 3 4 5 6 79 81 83 85 87 89 91 93 95 97 99 8 101 102 103 104 105 angmgmaddov1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( <" x y z "> .+ <" u v w "> ) = <" x y t "> )
107 77 106 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( E .+ F ) = <" x y t "> )
108 40 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> P e. _V )
109 104 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( v .- u ) = ( y .- t ) )
110 93 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> v =/= u )
111 1 4 3 79 83 81 89 102 109 110 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> y =/= t )
112 2 108 87 89 102 97 111 elcgrabasrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> <" x y t "> e. A )
113 107 112 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) /\ t e. P ) /\ ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) -> ( E .+ F ) e. A )
114 1 2 3 4 5 6 78 80 82 84 86 88 90 92 94 96 98 100 angmgmaddov1lem 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> E! s e. P ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) )
115 reurex 
 |-  ( E! s e. P ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) -> E. s e. P ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) )
116 114 115 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> E. s e. P ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) )
117 eqidd 
 |-  ( s = t -> z = z )
118 eqidd 
 |-  ( s = t -> y = y )
119 117 118 66 s3eqd 
 |-  ( s = t -> <" z y s "> = <" z y t "> )
120 119 breq1d 
 |-  ( s = t -> ( <" z y s "> .~ <" u v w "> <-> <" z y t "> .~ <" u v w "> ) )
121 oveq2 
 |-  ( s = t -> ( y .- s ) = ( y .- t ) )
122 121 eqeq1d 
 |-  ( s = t -> ( ( y .- s ) = ( v .- u ) <-> ( y .- t ) = ( v .- u ) ) )
123 oveq1 
 |-  ( s = t -> ( s I x ) = ( t I x ) )
124 123 ineq2d 
 |-  ( s = t -> ( ( y L z ) i^i ( s I x ) ) = ( ( y L z ) i^i ( t I x ) ) )
125 124 neeq1d 
 |-  ( s = t -> ( ( ( y L z ) i^i ( s I x ) ) =/= (/) <-> ( ( y L z ) i^i ( t I x ) ) =/= (/) ) )
126 120 122 125 3anbi123d 
 |-  ( s = t -> ( ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) <-> ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) ) )
127 126 cbvrexvw 
 |-  ( E. s e. P ( <" z y s "> .~ <" u v w "> /\ ( y .- s ) = ( v .- u ) /\ ( ( y L z ) i^i ( s I x ) ) =/= (/) ) <-> E. t e. P ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) )
128 116 127 sylib 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> E. t e. P ( <" z y t "> .~ <" u v w "> /\ ( y .- t ) = ( v .- u ) /\ ( ( y L z ) i^i ( t I x ) ) =/= (/) ) )
129 113 128 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. x e. ( y L z ) ) -> ( E .+ F ) e. A )
130 exmidd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( x e. ( y L z ) \/ -. x e. ( y L z ) ) )
131 74 129 130 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( E .+ F ) e. A )
132 131 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ F = <" u v w "> ) /\ ( u =/= v /\ v =/= w ) ) -> ( E .+ F ) e. A )
133 132 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ ( F = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( E .+ F ) e. A )
134 133 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ E. w e. P ( F = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( E .+ F ) e. A )
135 40 2 10 elcgrabasi 
 |-  ( ph -> E. u e. P E. v e. P E. w e. P ( F = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
136 135 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> E. u e. P E. v e. P E. w e. P ( F = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
137 134 136 r19.29vva 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> ( E .+ F ) e. A )
138 137 anasss 
 |-  ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ E = <" x y z "> ) /\ ( x =/= y /\ y =/= z ) ) -> ( E .+ F ) e. A )
139 138 anasss 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> ( E .+ F ) e. A )
140 139 r19.29an 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ E. z e. P ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> ( E .+ F ) e. A )
141 40 2 9 elcgrabasi 
 |-  ( ph -> E. x e. P E. y e. P E. z e. P ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )
142 140 141 r19.29vva 
 |-  ( ph -> ( E .+ F ) e. A )