Metamath Proof Explorer

Theorem 5oalem3

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

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

Proof

Step Hyp Ref Expression
1 5oalem3.1 
 |-  A e. SH
2 5oalem3.2 
 |-  B e. SH
3 5oalem3.3 
 |-  C e. SH
4 5oalem3.4 
 |-  D e. SH
5 5oalem3.5 
 |-  F e. SH
6 5oalem3.6 
 |-  G e. SH
7 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 ) ) ) )
8 1 2 5 6 5oalem2 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( x +h y ) = ( f +h g ) ) -> ( x -h f ) e. ( ( A +H F ) i^i ( B +H G ) ) )
9 3 4 5 6 5oalem2 
 |-  ( ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( z +h w ) = ( f +h g ) ) -> ( z -h f ) e. ( ( C +H F ) i^i ( D +H G ) ) )
10 8 9 anim12i 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( x +h y ) = ( f +h g ) ) /\ ( ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( ( x -h f ) e. ( ( A +H F ) i^i ( B +H G ) ) /\ ( z -h f ) e. ( ( C +H F ) i^i ( D +H G ) ) ) )
11 10 an4s 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( f e. F /\ g e. G ) ) /\ ( ( z e. C /\ w e. D ) /\ ( f e. F /\ g e. G ) ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( ( x -h f ) e. ( ( A +H F ) i^i ( B +H G ) ) /\ ( z -h f ) e. ( ( C +H F ) i^i ( D +H G ) ) ) )
12 7 11 sylanb 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( ( x -h f ) e. ( ( A +H F ) i^i ( B +H G ) ) /\ ( z -h f ) e. ( ( C +H F ) i^i ( D +H G ) ) ) )
13 1 5 shscli 
 |-  ( A +H F ) e. SH
14 2 6 shscli 
 |-  ( B +H G ) e. SH
15 13 14 shincli 
 |-  ( ( A +H F ) i^i ( B +H G ) ) e. SH
16 3 5 shscli 
 |-  ( C +H F ) e. SH
17 4 6 shscli 
 |-  ( D +H G ) e. SH
18 16 17 shincli 
 |-  ( ( C +H F ) i^i ( D +H G ) ) e. SH
19 15 18 shsvsi 
 |-  ( ( ( x -h f ) e. ( ( A +H F ) i^i ( B +H G ) ) /\ ( z -h f ) e. ( ( C +H F ) i^i ( D +H G ) ) ) -> ( ( x -h f ) -h ( z -h f ) ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) )
20 12 19 syl 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( ( x -h f ) -h ( z -h f ) ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) )
21 1 sheli 
 |-  ( x e. A -> x e. ~H )
22 21 adantr 
 |-  ( ( x e. A /\ y e. B ) -> x e. ~H )
23 3 sheli 
 |-  ( z e. C -> z e. ~H )
24 23 adantr 
 |-  ( ( z e. C /\ w e. D ) -> z e. ~H )
25 22 24 anim12i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) -> ( x e. ~H /\ z e. ~H ) )
26 5 sheli 
 |-  ( f e. F -> f e. ~H )
27 26 adantr 
 |-  ( ( f e. F /\ g e. G ) -> f e. ~H )
28 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 ) ) )
29 28 anandirs 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h f ) -h ( z -h f ) ) = ( ( x -h z ) -h ( f -h f ) ) )
30 hvsubid 
 |-  ( f e. ~H -> ( f -h f ) = 0h )
31 30 oveq2d 
 |-  ( f e. ~H -> ( ( x -h z ) -h ( f -h f ) ) = ( ( x -h z ) -h 0h ) )
32 hvsubcl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x -h z ) e. ~H )
33 hvsub0 
 |-  ( ( x -h z ) e. ~H -> ( ( x -h z ) -h 0h ) = ( x -h z ) )
34 32 33 syl 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( x -h z ) -h 0h ) = ( x -h z ) )
35 31 34 sylan9eqr 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h z ) -h ( f -h f ) ) = ( x -h z ) )
36 29 35 eqtrd 
 |-  ( ( ( x e. ~H /\ z e. ~H ) /\ f e. ~H ) -> ( ( x -h f ) -h ( z -h f ) ) = ( x -h z ) )
37 25 27 36 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 ) )
38 37 eleq1d 
 |-  ( ( ( ( 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 ) ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) <-> ( x -h z ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) ) )
39 38 adantr 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( ( ( x -h f ) -h ( z -h f ) ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) <-> ( x -h z ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) ) )
40 20 39 mpbid 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) )