Theorem 5oalem6

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	5oalem5.1	|- A e. SH
	5oalem5.2	|- B e. SH
	5oalem5.3	|- C e. SH
	5oalem5.4	|- D e. SH
	5oalem5.5	|- F e. SH
	5oalem5.6	|- G e. SH
	5oalem5.7	|- R e. SH
	5oalem5.8	|- S e. SH
Assertion	5oalem6	|- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		5oalem5.1	|- A e. SH
2		5oalem5.2	|- B e. SH
3		5oalem5.3	|- C e. SH
4		5oalem5.4	|- D e. SH
5		5oalem5.5	|- F e. SH
6		5oalem5.6	|- G e. SH
7		5oalem5.7	|- R e. SH
8		5oalem5.8	|- S e. SH
9		an4	|- ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) <-> ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( h = ( x +h y ) /\ h = ( z +h w ) ) ) )
10		an4	|- ( ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) <-> ( ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) /\ ( h = ( f +h g ) /\ h = ( v +h u ) ) ) )
11		eqeq1	|- ( h = ( x +h y ) -> ( h = ( v +h u ) <-> ( x +h y ) = ( v +h u ) ) )
12	11	biimpcd	|- ( h = ( v +h u ) -> ( h = ( x +h y ) -> ( x +h y ) = ( v +h u ) ) )
13		eqeq1	|- ( h = ( z +h w ) -> ( h = ( v +h u ) <-> ( z +h w ) = ( v +h u ) ) )
14	13	biimpcd	|- ( h = ( v +h u ) -> ( h = ( z +h w ) -> ( z +h w ) = ( v +h u ) ) )
15	12 14	anim12d	|- ( h = ( v +h u ) -> ( ( h = ( x +h y ) /\ h = ( z +h w ) ) -> ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) ) )
16		eqeq1	|- ( h = ( f +h g ) -> ( h = ( v +h u ) <-> ( f +h g ) = ( v +h u ) ) )
17	16	biimpcd	|- ( h = ( v +h u ) -> ( h = ( f +h g ) -> ( f +h g ) = ( v +h u ) ) )
18	15 17	anim12d	|- ( h = ( v +h u ) -> ( ( ( h = ( x +h y ) /\ h = ( z +h w ) ) /\ h = ( f +h g ) ) -> ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) )
19	18	expdcom	|- ( ( h = ( x +h y ) /\ h = ( z +h w ) ) -> ( h = ( f +h g ) -> ( h = ( v +h u ) -> ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) ) )
20	19	imp32	|- ( ( ( h = ( x +h y ) /\ h = ( z +h w ) ) /\ ( h = ( f +h g ) /\ h = ( v +h u ) ) ) -> ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) )
21	20	anim2i	|- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( h = ( x +h y ) /\ h = ( z +h w ) ) /\ ( h = ( f +h g ) /\ h = ( v +h u ) ) ) ) -> ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) )
22	21	an4s	|- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( h = ( x +h y ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) /\ ( h = ( f +h g ) /\ h = ( v +h u ) ) ) ) -> ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) )
23	9 10 22	syl2anb	|- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) )
24	1 2 3 4 5 6 7 8	5oalem5	|- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) -> ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) )
25	23 24	syl	|- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) )
26	1 3	shscli	|- ( A +H C ) e. SH
27	2 4	shscli	|- ( B +H D ) e. SH
28	26 27	shincli	|- ( ( A +H C ) i^i ( B +H D ) ) e. SH
29	1 7	shscli	|- ( A +H R ) e. SH
30	2 8	shscli	|- ( B +H S ) e. SH
31	29 30	shincli	|- ( ( A +H R ) i^i ( B +H S ) ) e. SH
32	3 7	shscli	|- ( C +H R ) e. SH
33	4 8	shscli	|- ( D +H S ) e. SH
34	32 33	shincli	|- ( ( C +H R ) i^i ( D +H S ) ) e. SH
35	31 34	shscli	|- ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) e. SH
36	28 35	shincli	|- ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) e. SH
37	1 5	shscli	|- ( A +H F ) e. SH
38	2 6	shscli	|- ( B +H G ) e. SH
39	37 38	shincli	|- ( ( A +H F ) i^i ( B +H G ) ) e. SH
40	5 7	shscli	|- ( F +H R ) e. SH
41	6 8	shscli	|- ( G +H S ) e. SH
42	40 41	shincli	|- ( ( F +H R ) i^i ( G +H S ) ) e. SH
43	31 42	shscli	|- ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
44	39 43	shincli	|- ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) e. SH
45	3 5	shscli	|- ( C +H F ) e. SH
46	4 6	shscli	|- ( D +H G ) e. SH
47	45 46	shincli	|- ( ( C +H F ) i^i ( D +H G ) ) e. SH
48	34 42	shscli	|- ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
49	47 48	shincli	|- ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) e. SH
50	44 49	shscli	|- ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) e. SH
51	36 50	shincli	|- ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) e. SH
52	1 2 3 51	5oalem1	|- ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
53	52	expr	|- ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ z e. C ) -> ( ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) ) )
54	53	adantrr	|- ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( z e. C /\ w e. D ) ) -> ( ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) ) )
55	54	adantrr	|- ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) -> ( ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) ) )
56	55	adantr	|- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> ( ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) ) )
57	25 56	mpd	|- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )