Metamath Proof Explorer

Theorem 5oalem2

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

Ref Expression
Hypotheses 5oalem2.1 
|- A e. SH
5oalem2.2 
|- B e. SH
5oalem2.3 
|- C e. SH
5oalem2.4 
|- D e. SH
Assertion 5oalem2 
|- ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )

Proof

Step Hyp Ref Expression
1 5oalem2.1 
 |-  A e. SH
2 5oalem2.2 
 |-  B e. SH
3 5oalem2.3 
 |-  C e. SH
4 5oalem2.4 
 |-  D e. SH
5 1 3 shsvsi 
 |-  ( ( x e. A /\ z e. C ) -> ( x -h z ) e. ( A +H C ) )
6 5 ad2ant2r 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) -> ( x -h z ) e. ( A +H C ) )
7 6 adantr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( A +H C ) )
8 4 2 shsvsi 
 |-  ( ( w e. D /\ y e. B ) -> ( w -h y ) e. ( D +H B ) )
9 8 ancoms 
 |-  ( ( y e. B /\ w e. D ) -> ( w -h y ) e. ( D +H B ) )
10 2 4 shscomi 
 |-  ( B +H D ) = ( D +H B )
11 9 10 eleqtrrdi 
 |-  ( ( y e. B /\ w e. D ) -> ( w -h y ) e. ( B +H D ) )
12 11 ad2ant2l 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) -> ( w -h y ) e. ( B +H D ) )
13 12 adantr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( w -h y ) e. ( B +H D ) )
14 1 sheli 
 |-  ( x e. A -> x e. ~H )
15 2 sheli 
 |-  ( y e. B -> y e. ~H )
16 14 15 anim12i 
 |-  ( ( x e. A /\ y e. B ) -> ( x e. ~H /\ y e. ~H ) )
17 3 sheli 
 |-  ( z e. C -> z e. ~H )
18 4 sheli 
 |-  ( w e. D -> w e. ~H )
19 17 18 anim12i 
 |-  ( ( z e. C /\ w e. D ) -> ( z e. ~H /\ w e. ~H ) )
20 16 19 anim12i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) -> ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )
21 oveq1 
 |-  ( ( x +h y ) = ( z +h w ) -> ( ( x +h y ) -h ( z +h y ) ) = ( ( z +h w ) -h ( z +h y ) ) )
22 21 adantl 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( ( x +h y ) -h ( z +h y ) ) = ( ( z +h w ) -h ( z +h y ) ) )
23 simpr 
 |-  ( ( x e. ~H /\ y e. ~H ) -> y e. ~H )
24 23 anim2i 
 |-  ( ( z e. ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( z e. ~H /\ y e. ~H ) )
25 24 ancoms 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( z e. ~H /\ y e. ~H ) )
26 hvsub4 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ y e. ~H ) ) -> ( ( x +h y ) -h ( z +h y ) ) = ( ( x -h z ) +h ( y -h y ) ) )
27 25 26 syldan 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( x +h y ) -h ( z +h y ) ) = ( ( x -h z ) +h ( y -h y ) ) )
28 hvsubid 
 |-  ( y e. ~H -> ( y -h y ) = 0h )
29 28 oveq2d 
 |-  ( y e. ~H -> ( ( x -h z ) +h ( y -h y ) ) = ( ( x -h z ) +h 0h ) )
30 29 ad2antlr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( x -h z ) +h ( y -h y ) ) = ( ( x -h z ) +h 0h ) )
31 hvsubcl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x -h z ) e. ~H )
32 ax-hvaddid 
 |-  ( ( x -h z ) e. ~H -> ( ( x -h z ) +h 0h ) = ( x -h z ) )
33 31 32 syl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( x -h z ) +h 0h ) = ( x -h z ) )
34 33 adantlr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( x -h z ) +h 0h ) = ( x -h z ) )
35 27 30 34 3eqtrd 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( x +h y ) -h ( z +h y ) ) = ( x -h z ) )
36 35 adantrr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) -h ( z +h y ) ) = ( x -h z ) )
37 36 adantr 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( ( x +h y ) -h ( z +h y ) ) = ( x -h z ) )
38 simpr 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( z e. ~H /\ w e. ~H ) )
39 simpl 
 |-  ( ( z e. ~H /\ w e. ~H ) -> z e. ~H )
40 39 anim1i 
 |-  ( ( ( z e. ~H /\ w e. ~H ) /\ y e. ~H ) -> ( z e. ~H /\ y e. ~H ) )
41 40 ancoms 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( z e. ~H /\ y e. ~H ) )
42 hvsub4 
 |-  ( ( ( z e. ~H /\ w e. ~H ) /\ ( z e. ~H /\ y e. ~H ) ) -> ( ( z +h w ) -h ( z +h y ) ) = ( ( z -h z ) +h ( w -h y ) ) )
43 38 41 42 syl2anc 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( z +h y ) ) = ( ( z -h z ) +h ( w -h y ) ) )
44 hvsubid 
 |-  ( z e. ~H -> ( z -h z ) = 0h )
45 44 oveq1d 
 |-  ( z e. ~H -> ( ( z -h z ) +h ( w -h y ) ) = ( 0h +h ( w -h y ) ) )
46 45 ad2antrl 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z -h z ) +h ( w -h y ) ) = ( 0h +h ( w -h y ) ) )
47 hvsubcl 
 |-  ( ( w e. ~H /\ y e. ~H ) -> ( w -h y ) e. ~H )
48 hvaddid2 
 |-  ( ( w -h y ) e. ~H -> ( 0h +h ( w -h y ) ) = ( w -h y ) )
49 47 48 syl 
 |-  ( ( w e. ~H /\ y e. ~H ) -> ( 0h +h ( w -h y ) ) = ( w -h y ) )
50 49 ancoms 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( 0h +h ( w -h y ) ) = ( w -h y ) )
51 50 adantrl 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( 0h +h ( w -h y ) ) = ( w -h y ) )
52 43 46 51 3eqtrd 
 |-  ( ( y e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( z +h y ) ) = ( w -h y ) )
53 52 adantll 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( z +h y ) ) = ( w -h y ) )
54 53 adantr 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( ( z +h w ) -h ( z +h y ) ) = ( w -h y ) )
55 22 37 54 3eqtr3d 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) = ( w -h y ) )
56 55 eleq1d 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( ( x -h z ) e. ( B +H D ) <-> ( w -h y ) e. ( B +H D ) ) )
57 20 56 sylan 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( ( x -h z ) e. ( B +H D ) <-> ( w -h y ) e. ( B +H D ) ) )
58 13 57 mpbird 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( B +H D ) )
59 7 58 elind 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )