Metamath Proof Explorer


Theorem 3oalem2

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses 3oalem1.1
|- B e. CH
3oalem1.2
|- C e. CH
3oalem1.3
|- R e. CH
3oalem1.4
|- S e. CH
Assertion 3oalem2
|- ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 3oalem1.1
 |-  B e. CH
2 3oalem1.2
 |-  C e. CH
3 3oalem1.3
 |-  R e. CH
4 3oalem1.4
 |-  S e. CH
5 simplll
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> x e. B )
6 simpllr
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. R )
7 1 2 3 4 3oalem1
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )
8 hvaddsub12
 |-  ( ( y e. ~H /\ w e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = ( w +h ( y -h w ) ) )
9 8 3anidm23
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = ( w +h ( y -h w ) ) )
10 hvsubid
 |-  ( w e. ~H -> ( w -h w ) = 0h )
11 10 oveq2d
 |-  ( w e. ~H -> ( y +h ( w -h w ) ) = ( y +h 0h ) )
12 ax-hvaddid
 |-  ( y e. ~H -> ( y +h 0h ) = y )
13 11 12 sylan9eqr
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = y )
14 9 13 eqtr3d
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( w +h ( y -h w ) ) = y )
15 14 ad2ant2l
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( w +h ( y -h w ) ) = y )
16 15 adantlr
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( w +h ( y -h w ) ) = y )
17 7 16 syl
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( w +h ( y -h w ) ) = y )
18 simprlr
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> w e. S )
19 eqtr2
 |-  ( ( v = ( x +h y ) /\ v = ( z +h w ) ) -> ( x +h y ) = ( z +h w ) )
20 19 oveq1d
 |-  ( ( v = ( x +h y ) /\ v = ( z +h w ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( z +h w ) -h ( x +h w ) ) )
21 20 ad2ant2l
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( z +h w ) -h ( x +h w ) ) )
22 simpl
 |-  ( ( x e. ~H /\ y e. ~H ) -> x e. ~H )
23 22 anim1i
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( x e. ~H /\ w e. ~H ) )
24 hvsub4
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( x -h x ) +h ( y -h w ) ) )
25 23 24 syldan
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( x -h x ) +h ( y -h w ) ) )
26 hvsubid
 |-  ( x e. ~H -> ( x -h x ) = 0h )
27 26 ad2antrr
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( x -h x ) = 0h )
28 27 oveq1d
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x -h x ) +h ( y -h w ) ) = ( 0h +h ( y -h w ) ) )
29 hvsubcl
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y -h w ) e. ~H )
30 hvaddid2
 |-  ( ( y -h w ) e. ~H -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
31 29 30 syl
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
32 31 adantll
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
33 25 28 32 3eqtrd
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
34 33 ad2ant2rl
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
35 7 34 syl
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
36 simpr
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( z e. ~H /\ w e. ~H ) )
37 simpr
 |-  ( ( z e. ~H /\ w e. ~H ) -> w e. ~H )
38 37 anim2i
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( x e. ~H /\ w e. ~H ) )
39 hvsub4
 |-  ( ( ( z e. ~H /\ w e. ~H ) /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( ( z -h x ) +h ( w -h w ) ) )
40 36 38 39 syl2anc
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( ( z -h x ) +h ( w -h w ) ) )
41 10 ad2antll
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( w -h w ) = 0h )
42 41 oveq2d
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z -h x ) +h ( w -h w ) ) = ( ( z -h x ) +h 0h ) )
43 hvsubcl
 |-  ( ( z e. ~H /\ x e. ~H ) -> ( z -h x ) e. ~H )
44 ax-hvaddid
 |-  ( ( z -h x ) e. ~H -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
45 43 44 syl
 |-  ( ( z e. ~H /\ x e. ~H ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
46 45 ancoms
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
47 46 adantrr
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
48 40 42 47 3eqtrd
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
49 48 adantlr
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
50 49 adantlr
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
51 7 50 syl
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
52 21 35 51 3eqtr3d
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) = ( z -h x ) )
53 simpll
 |-  ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) -> x e. B )
54 simpll
 |-  ( ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) -> z e. C )
55 2 chshii
 |-  C e. SH
56 1 chshii
 |-  B e. SH
57 55 56 shsvsi
 |-  ( ( z e. C /\ x e. B ) -> ( z -h x ) e. ( C +H B ) )
58 57 ancoms
 |-  ( ( x e. B /\ z e. C ) -> ( z -h x ) e. ( C +H B ) )
59 56 55 shscomi
 |-  ( B +H C ) = ( C +H B )
60 58 59 eleqtrrdi
 |-  ( ( x e. B /\ z e. C ) -> ( z -h x ) e. ( B +H C ) )
61 53 54 60 syl2an
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( z -h x ) e. ( B +H C ) )
62 52 61 eqeltrd
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( B +H C ) )
63 simplr
 |-  ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) -> y e. R )
64 simplr
 |-  ( ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) -> w e. S )
65 3 chshii
 |-  R e. SH
66 4 chshii
 |-  S e. SH
67 65 66 shsvsi
 |-  ( ( y e. R /\ w e. S ) -> ( y -h w ) e. ( R +H S ) )
68 63 64 67 syl2an
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( R +H S ) )
69 62 68 elind
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( ( B +H C ) i^i ( R +H S ) ) )
70 56 55 shscli
 |-  ( B +H C ) e. SH
71 65 66 shscli
 |-  ( R +H S ) e. SH
72 70 71 shincli
 |-  ( ( B +H C ) i^i ( R +H S ) ) e. SH
73 66 72 shsvai
 |-  ( ( w e. S /\ ( y -h w ) e. ( ( B +H C ) i^i ( R +H S ) ) ) -> ( w +h ( y -h w ) ) e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
74 18 69 73 syl2anc
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( w +h ( y -h w ) ) e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
75 17 74 eqeltrrd
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
76 6 75 elind
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) )
77 66 72 shscli
 |-  ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) e. SH
78 65 77 shincli
 |-  ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) e. SH
79 56 78 shsvai
 |-  ( ( x e. B /\ y e. ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) -> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )
80 5 76 79 syl2anc
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )
81 eleq1
 |-  ( v = ( x +h y ) -> ( v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) <-> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) ) )
82 81 ad2antlr
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) <-> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) ) )
83 80 82 mpbird
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )