Theorem axtg5seg

Description: Five segments axiom, Axiom A5 of Schwabhauser p. 11. Take two triangles X Z U and A C V , a point Y on X Z , and a point B on A C . If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .A B , Y Z .B C , X U .A V , and Y U .B V ), then Z U and C V are also congruent. As noted in Axiom 5 of Tarski1999 p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	|- P = ( Base ` G )
	axtrkg.d	|- .- = ( dist ` G )
	axtrkg.i	|- I = ( Itv ` G )
	axtrkg.g	|- ( ph -> G e. TarskiG )
	axtg5seg.1	|- ( ph -> X e. P )
	axtg5seg.2	|- ( ph -> Y e. P )
	axtg5seg.3	|- ( ph -> Z e. P )
	axtg5seg.4	|- ( ph -> A e. P )
	axtg5seg.5	|- ( ph -> B e. P )
	axtg5seg.6	|- ( ph -> C e. P )
	axtg5seg.7	|- ( ph -> U e. P )
	axtg5seg.8	|- ( ph -> V e. P )
	axtg5seg.9	|- ( ph -> X =/= Y )
	axtg5seg.10	|- ( ph -> Y e. ( X I Z ) )
	axtg5seg.11	|- ( ph -> B e. ( A I C ) )
	axtg5seg.12	|- ( ph -> ( X .- Y ) = ( A .- B ) )
	axtg5seg.13	|- ( ph -> ( Y .- Z ) = ( B .- C ) )
	axtg5seg.14	|- ( ph -> ( X .- U ) = ( A .- V ) )
	axtg5seg.15	|- ( ph -> ( Y .- U ) = ( B .- V ) )
Assertion	axtg5seg	|- ( ph -> ( Z .- U ) = ( C .- V ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	|- P = ( Base ` G )
2		axtrkg.d	|- .- = ( dist ` G )
3		axtrkg.i	|- I = ( Itv ` G )
4		axtrkg.g	|- ( ph -> G e. TarskiG )
5		axtg5seg.1	|- ( ph -> X e. P )
6		axtg5seg.2	|- ( ph -> Y e. P )
7		axtg5seg.3	|- ( ph -> Z e. P )
8		axtg5seg.4	|- ( ph -> A e. P )
9		axtg5seg.5	|- ( ph -> B e. P )
10		axtg5seg.6	|- ( ph -> C e. P )
11		axtg5seg.7	|- ( ph -> U e. P )
12		axtg5seg.8	|- ( ph -> V e. P )
13		axtg5seg.9	|- ( ph -> X =/= Y )
14		axtg5seg.10	|- ( ph -> Y e. ( X I Z ) )
15		axtg5seg.11	|- ( ph -> B e. ( A I C ) )
16		axtg5seg.12	|- ( ph -> ( X .- Y ) = ( A .- B ) )
17		axtg5seg.13	|- ( ph -> ( Y .- Z ) = ( B .- C ) )
18		axtg5seg.14	|- ( ph -> ( X .- U ) = ( A .- V ) )
19		axtg5seg.15	|- ( ph -> ( Y .- U ) = ( B .- V ) )
20		df-trkg	|- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
21		inss2	|- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } )
22		inss1	|- ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) C_ TarskiGCB
23	21 22	sstri	|- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGCB
24	20 23	eqsstri	|- TarskiG C_ TarskiGCB
25	24 4	sseldi	|- ( ph -> G e. TarskiGCB )
26	1 2 3	istrkgcb	|- ( G e. TarskiGCB <-> ( G e. _V /\ ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )
27	26	simprbi	|- ( G e. TarskiGCB -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) )
28	27	simpld	|- ( G e. TarskiGCB -> A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) )
29	25 28	syl	|- ( ph -> A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) )
30		neeq1	|- ( x = X -> ( x =/= y <-> X =/= y ) )
31		oveq1	|- ( x = X -> ( x I z ) = ( X I z ) )
32	31	eleq2d	|- ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
33	30 32	3anbi12d	|- ( x = X -> ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) <-> ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) ) )
34		oveq1	|- ( x = X -> ( x .- y ) = ( X .- y ) )
35	34	eqeq1d	|- ( x = X -> ( ( x .- y ) = ( a .- b ) <-> ( X .- y ) = ( a .- b ) ) )
36	35	anbi1d	|- ( x = X -> ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) <-> ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) ) )
37		oveq1	|- ( x = X -> ( x .- u ) = ( X .- u ) )
38	37	eqeq1d	|- ( x = X -> ( ( x .- u ) = ( a .- v ) <-> ( X .- u ) = ( a .- v ) ) )
39	38	anbi1d	|- ( x = X -> ( ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) <-> ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) )
40	36 39	anbi12d	|- ( x = X -> ( ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) )
41	33 40	anbi12d	|- ( x = X -> ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) <-> ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) ) )
42	41	imbi1d	|- ( x = X -> ( ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
43	42	ralbidv	|- ( x = X -> ( A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
44	43	2ralbidv	|- ( x = X -> ( A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. b e. P A. c e. P A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
45	44	2ralbidv	|- ( x = X -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
46		neeq2	|- ( y = Y -> ( X =/= y <-> X =/= Y ) )
47		eleq1	|- ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
48	46 47	3anbi12d	|- ( y = Y -> ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) ) )
49		oveq2	|- ( y = Y -> ( X .- y ) = ( X .- Y ) )
50	49	eqeq1d	|- ( y = Y -> ( ( X .- y ) = ( a .- b ) <-> ( X .- Y ) = ( a .- b ) ) )
51		oveq1	|- ( y = Y -> ( y .- z ) = ( Y .- z ) )
52	51	eqeq1d	|- ( y = Y -> ( ( y .- z ) = ( b .- c ) <-> ( Y .- z ) = ( b .- c ) ) )
53	50 52	anbi12d	|- ( y = Y -> ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) ) )
54		oveq1	|- ( y = Y -> ( y .- u ) = ( Y .- u ) )
55	54	eqeq1d	|- ( y = Y -> ( ( y .- u ) = ( b .- v ) <-> ( Y .- u ) = ( b .- v ) ) )
56	55	anbi2d	|- ( y = Y -> ( ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) <-> ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) )
57	53 56	anbi12d	|- ( y = Y -> ( ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) )
58	48 57	anbi12d	|- ( y = Y -> ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) ) )
59	58	imbi1d	|- ( y = Y -> ( ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
60	59	ralbidv	|- ( y = Y -> ( A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
61	60	2ralbidv	|- ( y = Y -> ( A. b e. P A. c e. P A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
62	61	2ralbidv	|- ( y = Y -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) ) )
63		oveq2	|- ( z = Z -> ( X I z ) = ( X I Z ) )
64	63	eleq2d	|- ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
65	64	3anbi2d	|- ( z = Z -> ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) ) )
66		oveq2	|- ( z = Z -> ( Y .- z ) = ( Y .- Z ) )
67	66	eqeq1d	|- ( z = Z -> ( ( Y .- z ) = ( b .- c ) <-> ( Y .- Z ) = ( b .- c ) ) )
68	67	anbi2d	|- ( z = Z -> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) ) )
69	68	anbi1d	|- ( z = Z -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) )
70	65 69	anbi12d	|- ( z = Z -> ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) ) )
71		oveq1	|- ( z = Z -> ( z .- u ) = ( Z .- u ) )
72	71	eqeq1d	|- ( z = Z -> ( ( z .- u ) = ( c .- v ) <-> ( Z .- u ) = ( c .- v ) ) )
73	70 72	imbi12d	|- ( z = Z -> ( ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
74	73	ralbidv	|- ( z = Z -> ( A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
75	74	2ralbidv	|- ( z = Z -> ( A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
76	75	2ralbidv	|- ( z = Z -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
77	45 62 76	rspc3v	|- ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) -> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
78	5 6 7 77	syl3anc	|- ( ph -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) -> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) ) )
79	29 78	mpd	|- ( ph -> A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) )
80		oveq2	|- ( u = U -> ( X .- u ) = ( X .- U ) )
81	80	eqeq1d	|- ( u = U -> ( ( X .- u ) = ( a .- v ) <-> ( X .- U ) = ( a .- v ) ) )
82		oveq2	|- ( u = U -> ( Y .- u ) = ( Y .- U ) )
83	82	eqeq1d	|- ( u = U -> ( ( Y .- u ) = ( b .- v ) <-> ( Y .- U ) = ( b .- v ) ) )
84	81 83	anbi12d	|- ( u = U -> ( ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) <-> ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) )
85	84	anbi2d	|- ( u = U -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) )
86	85	anbi2d	|- ( u = U -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) ) )
87		oveq2	|- ( u = U -> ( Z .- u ) = ( Z .- U ) )
88	87	eqeq1d	|- ( u = U -> ( ( Z .- u ) = ( c .- v ) <-> ( Z .- U ) = ( c .- v ) ) )
89	86 88	imbi12d	|- ( u = U -> ( ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
90	89	2ralbidv	|- ( u = U -> ( A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) <-> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
91		oveq1	|- ( a = A -> ( a I c ) = ( A I c ) )
92	91	eleq2d	|- ( a = A -> ( b e. ( a I c ) <-> b e. ( A I c ) ) )
93	92	3anbi3d	|- ( a = A -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) ) )
94		oveq1	|- ( a = A -> ( a .- b ) = ( A .- b ) )
95	94	eqeq2d	|- ( a = A -> ( ( X .- Y ) = ( a .- b ) <-> ( X .- Y ) = ( A .- b ) ) )
96	95	anbi1d	|- ( a = A -> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) ) )
97		oveq1	|- ( a = A -> ( a .- v ) = ( A .- v ) )
98	97	eqeq2d	|- ( a = A -> ( ( X .- U ) = ( a .- v ) <-> ( X .- U ) = ( A .- v ) ) )
99	98	anbi1d	|- ( a = A -> ( ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) <-> ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) )
100	96 99	anbi12d	|- ( a = A -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) )
101	93 100	anbi12d	|- ( a = A -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) ) )
102	101	imbi1d	|- ( a = A -> ( ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
103	102	2ralbidv	|- ( a = A -> ( A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) <-> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
104		eleq1	|- ( b = B -> ( b e. ( A I c ) <-> B e. ( A I c ) ) )
105	104	3anbi3d	|- ( b = B -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) ) )
106		oveq2	|- ( b = B -> ( A .- b ) = ( A .- B ) )
107	106	eqeq2d	|- ( b = B -> ( ( X .- Y ) = ( A .- b ) <-> ( X .- Y ) = ( A .- B ) ) )
108		oveq1	|- ( b = B -> ( b .- c ) = ( B .- c ) )
109	108	eqeq2d	|- ( b = B -> ( ( Y .- Z ) = ( b .- c ) <-> ( Y .- Z ) = ( B .- c ) ) )
110	107 109	anbi12d	|- ( b = B -> ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) ) )
111		oveq1	|- ( b = B -> ( b .- v ) = ( B .- v ) )
112	111	eqeq2d	|- ( b = B -> ( ( Y .- U ) = ( b .- v ) <-> ( Y .- U ) = ( B .- v ) ) )
113	112	anbi2d	|- ( b = B -> ( ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) <-> ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) )
114	110 113	anbi12d	|- ( b = B -> ( ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) )
115	105 114	anbi12d	|- ( b = B -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) ) )
116	115	imbi1d	|- ( b = B -> ( ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
117	116	2ralbidv	|- ( b = B -> ( A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) <-> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
118	90 103 117	rspc3v	|- ( ( U e. P /\ A e. P /\ B e. P ) -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) -> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
119	11 8 9 118	syl3anc	|- ( ph -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) /\ ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) -> ( Z .- u ) = ( c .- v ) ) -> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) ) )
120	79 119	mpd	|- ( ph -> A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) )
121	13 14 15	3jca	|- ( ph -> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) )
122	16 17	jca	|- ( ph -> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) )
123	18 19	jca	|- ( ph -> ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) )
124	121 122 123	jca32	|- ( ph -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) )
125		oveq2	|- ( c = C -> ( A I c ) = ( A I C ) )
126	125	eleq2d	|- ( c = C -> ( B e. ( A I c ) <-> B e. ( A I C ) ) )
127	126	3anbi3d	|- ( c = C -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) ) )
128		oveq2	|- ( c = C -> ( B .- c ) = ( B .- C ) )
129	128	eqeq2d	|- ( c = C -> ( ( Y .- Z ) = ( B .- c ) <-> ( Y .- Z ) = ( B .- C ) ) )
130	129	anbi2d	|- ( c = C -> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) <-> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) ) )
131	130	anbi1d	|- ( c = C -> ( ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) )
132	127 131	anbi12d	|- ( c = C -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) ) )
133		oveq1	|- ( c = C -> ( c .- v ) = ( C .- v ) )
134	133	eqeq2d	|- ( c = C -> ( ( Z .- U ) = ( c .- v ) <-> ( Z .- U ) = ( C .- v ) ) )
135	132 134	imbi12d	|- ( c = C -> ( ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( C .- v ) ) ) )
136		oveq2	|- ( v = V -> ( A .- v ) = ( A .- V ) )
137	136	eqeq2d	|- ( v = V -> ( ( X .- U ) = ( A .- v ) <-> ( X .- U ) = ( A .- V ) ) )
138		oveq2	|- ( v = V -> ( B .- v ) = ( B .- V ) )
139	138	eqeq2d	|- ( v = V -> ( ( Y .- U ) = ( B .- v ) <-> ( Y .- U ) = ( B .- V ) ) )
140	137 139	anbi12d	|- ( v = V -> ( ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) <-> ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) )
141	140	anbi2d	|- ( v = V -> ( ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) )
142	141	anbi2d	|- ( v = V -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) <-> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) ) )
143		oveq2	|- ( v = V -> ( C .- v ) = ( C .- V ) )
144	143	eqeq2d	|- ( v = V -> ( ( Z .- U ) = ( C .- v ) <-> ( Z .- U ) = ( C .- V ) ) )
145	142 144	imbi12d	|- ( v = V -> ( ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( C .- v ) ) <-> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) -> ( Z .- U ) = ( C .- V ) ) ) )
146	135 145	rspc2v	|- ( ( C e. P /\ V e. P ) -> ( A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) -> ( Z .- U ) = ( C .- V ) ) ) )
147	10 12 146	syl2anc	|- ( ph -> ( A. c e. P A. v e. P ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) -> ( Z .- U ) = ( c .- v ) ) -> ( ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) /\ ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) -> ( Z .- U ) = ( C .- V ) ) ) )
148	120 124 147	mp2d	|- ( ph -> ( Z .- U ) = ( C .- V ) )