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 C
3oalem1.2 C C
3oalem1.3 R C
3oalem1.4 S C
Assertion 3oalem2 x B y R v = x + y z C w S v = z + w v B + R S + B + C R + S

Proof

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