Metamath Proof Explorer

Theorem 5oalem5

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-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 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 ) ) ) ) ) ) )

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 simpr 
 |-  ( ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) -> ( v e. R /\ u e. S ) )
10 9 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 ) ) ) -> ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( v e. R /\ u e. S ) ) )
11 simpl 
 |-  ( ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) -> ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) )
12 1 2 3 4 7 8 5oalem4 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( 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 ) ) ) ) )
13 10 11 12 syl2an 
 |-  ( ( ( ( ( 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 ) ) ) ) )
14 1 sheli 
 |-  ( x e. A -> x e. ~H )
15 14 adantr 
 |-  ( ( x e. A /\ y e. B ) -> x e. ~H )
16 3 sheli 
 |-  ( z e. C -> z e. ~H )
17 16 adantr 
 |-  ( ( z e. C /\ w e. D ) -> z e. ~H )
18 15 17 anim12i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) -> ( x e. ~H /\ z e. ~H ) )
19 5 sheli 
 |-  ( f e. F -> f e. ~H )
20 19 adantr 
 |-  ( ( f e. F /\ g e. G ) -> f e. ~H )
21 hvsubsub4 
 |-  ( ( ( x e. ~H /\ f e. ~H ) /\ ( z e. ~H /\ f e. ~H ) ) -> ( ( x -h f ) -h ( z -h f ) ) = ( ( x -h z ) -h ( f -h f ) ) )
22 21 anandirs 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h f ) -h ( z -h f ) ) = ( ( x -h z ) -h ( f -h f ) ) )
23 hvsubid 
 |-  ( f e. ~H -> ( f -h f ) = 0h )
24 23 oveq2d 
 |-  ( f e. ~H -> ( ( x -h z ) -h ( f -h f ) ) = ( ( x -h z ) -h 0h ) )
25 hvsubcl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x -h z ) e. ~H )
26 hvsub0 
 |-  ( ( x -h z ) e. ~H -> ( ( x -h z ) -h 0h ) = ( x -h z ) )
27 25 26 syl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( x -h z ) -h 0h ) = ( x -h z ) )
28 24 27 sylan9eqr 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h z ) -h ( f -h f ) ) = ( x -h z ) )
29 22 28 eqtrd 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h f ) -h ( z -h f ) ) = ( x -h z ) )
30 18 20 29 syl2an 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) -> ( ( x -h f ) -h ( z -h f ) ) = ( x -h z ) )
31 30 adantrr 
 |-  ( ( ( ( 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 f ) -h ( z -h f ) ) = ( x -h z ) )
32 31 adantr 
 |-  ( ( ( ( ( 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 f ) -h ( z -h f ) ) = ( x -h z ) )
33 simpl 
 |-  ( ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) -> ( f e. F /\ g e. G ) )
34 33 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 ) ) ) -> ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) )
35 anandir 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) <-> ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) )
36 34 35 sylib 
 |-  ( ( ( ( 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 e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) )
37 simprr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) -> ( v e. R /\ u e. S ) )
38 36 37 jca 
 |-  ( ( ( ( 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 e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) /\ ( v e. R /\ u e. S ) ) )
39 simpl 
 |-  ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) -> ( x +h y ) = ( v +h u ) )
40 39 anim1i 
 |-  ( ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) -> ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) )
41 simpr 
 |-  ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) -> ( z +h w ) = ( v +h u ) )
42 41 anim1i 
 |-  ( ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) -> ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) )
43 40 42 jca 
 |-  ( ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) -> ( ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) /\ ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) )
44 anandir 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) /\ ( v e. R /\ u e. S ) ) <-> ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) ) )
45 1 2 5 6 7 8 5oalem4 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) -> ( x -h f ) e. ( ( ( 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 ) ) ) ) )
46 3 4 5 6 7 8 5oalem4 
 |-  ( ( ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) -> ( z -h f ) e. ( ( ( 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 ) ) ) ) )
47 45 46 anim12i 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) /\ ( ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) ) -> ( ( x -h f ) e. ( ( ( 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 ) ) ) ) /\ ( z -h f ) e. ( ( ( 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 ) ) ) ) ) )
48 47 an4s 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) /\ ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) ) -> ( ( x -h f ) e. ( ( ( 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 ) ) ) ) /\ ( z -h f ) e. ( ( ( 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 ) ) ) ) ) )
49 44 48 sylanb 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) /\ ( v e. R /\ u e. S ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) /\ ( ( z +h w ) = ( v +h u ) /\ ( f +h g ) = ( v +h u ) ) ) ) -> ( ( x -h f ) e. ( ( ( 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 ) ) ) ) /\ ( z -h f ) e. ( ( ( 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 ) ) ) ) ) )
50 38 43 49 syl2an 
 |-  ( ( ( ( ( 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 f ) e. ( ( ( 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 ) ) ) ) /\ ( z -h f ) e. ( ( ( 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 ) ) ) ) ) )
51 1 5 shscli 
 |-  ( A +H F ) e. SH
52 2 6 shscli 
 |-  ( B +H G ) e. SH
53 51 52 shincli 
 |-  ( ( A +H F ) i^i ( B +H G ) ) e. SH
54 1 7 shscli 
 |-  ( A +H R ) e. SH
55 2 8 shscli 
 |-  ( B +H S ) e. SH
56 54 55 shincli 
 |-  ( ( A +H R ) i^i ( B +H S ) ) e. SH
57 5 7 shscli 
 |-  ( F +H R ) e. SH
58 6 8 shscli 
 |-  ( G +H S ) e. SH
59 57 58 shincli 
 |-  ( ( F +H R ) i^i ( G +H S ) ) e. SH
60 56 59 shscli 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
61 53 60 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
62 3 5 shscli 
 |-  ( C +H F ) e. SH
63 4 6 shscli 
 |-  ( D +H G ) e. SH
64 62 63 shincli 
 |-  ( ( C +H F ) i^i ( D +H G ) ) e. SH
65 3 7 shscli 
 |-  ( C +H R ) e. SH
66 4 8 shscli 
 |-  ( D +H S ) e. SH
67 65 66 shincli 
 |-  ( ( C +H R ) i^i ( D +H S ) ) e. SH
68 67 59 shscli 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
69 64 68 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
70 61 69 shsvsi 
 |-  ( ( ( x -h f ) e. ( ( ( 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 ) ) ) ) /\ ( z -h f ) e. ( ( ( 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 ) ) ) ) ) -> ( ( x -h f ) -h ( z -h f ) ) e. ( ( ( ( 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 ) ) ) ) ) )
71 50 70 syl 
 |-  ( ( ( ( ( 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 f ) -h ( z -h f ) ) e. ( ( ( ( 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 ) ) ) ) ) )
72 32 71 eqeltrrd 
 |-  ( ( ( ( ( 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 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 ) ) ) ) ) )
73 13 72 elind 
 |-  ( ( ( ( ( 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 ) ) ) ) ) ) )