Metamath Proof Explorer


Theorem mayete3i

Description: Mayet's equation E_3. Part of Theorem 4.1 of Mayet3 p. 1223. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mayete3.a A C
mayete3.b B C
mayete3.c C C
mayete3.d D C
mayete3.f F C
mayete3.g G C
mayete3.ac A C
mayete3.af A F
mayete3.cf C F
mayete3.ab A B
mayete3.cd C D
mayete3.fg F G
mayete3.x X = A C F
mayete3.y Y = A B C D F G
mayete3.z Z = B D G
Assertion mayete3i X Y Z

Proof

Step Hyp Ref Expression
1 mayete3.a A C
2 mayete3.b B C
3 mayete3.c C C
4 mayete3.d D C
5 mayete3.f F C
6 mayete3.g G C
7 mayete3.ac A C
8 mayete3.af A F
9 mayete3.cf C F
10 mayete3.ab A B
11 mayete3.cd C D
12 mayete3.fg F G
13 mayete3.x X = A C F
14 mayete3.y Y = A B C D F G
15 mayete3.z Z = B D G
16 elin x X Y x X x Y
17 1 3 chjcli A C C
18 17 5 chjcli A C F C
19 18 cheli x A C F x
20 19 13 eleq2s x X x
21 20 adantr x X x Y x
22 16 21 sylbi x X Y x
23 ax-hvmulid x 1 x = x
24 2cn 2
25 2ne0 2 0
26 recid2 2 2 0 1 2 2 = 1
27 24 25 26 mp2an 1 2 2 = 1
28 27 oveq1i 1 2 2 x = 1 x
29 halfcn 1 2
30 ax-hvmulass 1 2 2 x 1 2 2 x = 1 2 2 x
31 29 24 30 mp3an12 x 1 2 2 x = 1 2 2 x
32 28 31 eqtr3id x 1 x = 1 2 2 x
33 23 32 eqtr3d x x = 1 2 2 x
34 22 33 syl x X Y x = 1 2 2 x
35 hv2times x 2 x = x + x
36 35 oveq1d x 2 x + x = x + x + x
37 22 36 syl x X Y 2 x + x = x + x + x
38 inss2 X Y Y
39 38 sseli x X Y x Y
40 14 elin2 x Y x A B C D x F G
41 elin x A B C D x A B x C D
42 1 2 pjdsi x A B A B x = proj A x + proj B x
43 10 42 mpan2 x A B x = proj A x + proj B x
44 3 4 pjdsi x C D C D x = proj C x + proj D x
45 11 44 mpan2 x C D x = proj C x + proj D x
46 43 45 oveqan12d x A B x C D x + x = proj A x + proj B x + proj C x + proj D x
47 41 46 sylbi x A B C D x + x = proj A x + proj B x + proj C x + proj D x
48 inss1 A B C D A B
49 48 sseli x A B C D x A B
50 1 2 chjcli A B C
51 50 cheli x A B x
52 1 pjhcli x proj A x
53 2 pjhcli x proj B x
54 3 pjhcli x proj C x
55 4 pjhcli x proj D x
56 hvadd4 proj A x proj B x proj C x proj D x proj A x + proj B x + proj C x + proj D x = proj A x + proj C x + proj B x + proj D x
57 52 53 54 55 56 syl22anc x proj A x + proj B x + proj C x + proj D x = proj A x + proj C x + proj B x + proj D x
58 49 51 57 3syl x A B C D proj A x + proj B x + proj C x + proj D x = proj A x + proj C x + proj B x + proj D x
59 47 58 eqtrd x A B C D x + x = proj A x + proj C x + proj B x + proj D x
60 5 6 pjdsi x F G F G x = proj F x + proj G x
61 12 60 mpan2 x F G x = proj F x + proj G x
62 59 61 oveqan12d x A B C D x F G x + x + x = proj A x + proj C x + proj B x + proj D x + proj F x + proj G x
63 40 62 sylbi x Y x + x + x = proj A x + proj C x + proj B x + proj D x + proj F x + proj G x
64 39 63 syl x X Y x + x + x = proj A x + proj C x + proj B x + proj D x + proj F x + proj G x
65 hvaddcl proj A x proj C x proj A x + proj C x
66 52 54 65 syl2anc x proj A x + proj C x
67 hvaddcl proj B x proj D x proj B x + proj D x
68 53 55 67 syl2anc x proj B x + proj D x
69 5 pjhcli x proj F x
70 6 pjhcli x proj G x
71 hvadd4 proj A x + proj C x proj B x + proj D x proj F x proj G x proj A x + proj C x + proj B x + proj D x + proj F x + proj G x = proj A x + proj C x + proj F x + proj B x + proj D x + proj G x
72 66 68 69 70 71 syl22anc x proj A x + proj C x + proj B x + proj D x + proj F x + proj G x = proj A x + proj C x + proj F x + proj B x + proj D x + proj G x
73 22 72 syl x X Y proj A x + proj C x + proj B x + proj D x + proj F x + proj G x = proj A x + proj C x + proj F x + proj B x + proj D x + proj G x
74 37 64 73 3eqtrd x X Y 2 x + x = proj A x + proj C x + proj F x + proj B x + proj D x + proj G x
75 inss1 X Y X
76 75 sseli x X Y x X
77 76 13 eleqtrdi x X Y x A C F
78 1 3 5 pjds3i x A C F A C A F C F x = proj A x + proj C x + proj F x
79 8 9 78 mpanr12 x A C F A C x = proj A x + proj C x + proj F x
80 77 7 79 sylancl x X Y x = proj A x + proj C x + proj F x
81 74 80 oveq12d x X Y 2 x + x - x = proj A x + proj C x + proj F x + proj B x + proj D x + proj G x - proj A x + proj C x + proj F x
82 hvmulcl 2 x 2 x
83 24 82 mpan x 2 x
84 hvpncan 2 x x 2 x + x - x = 2 x
85 83 84 mpancom x 2 x + x - x = 2 x
86 22 85 syl x X Y 2 x + x - x = 2 x
87 81 86 eqtr3d x X Y proj A x + proj C x + proj F x + proj B x + proj D x + proj G x - proj A x + proj C x + proj F x = 2 x
88 hvaddcl proj A x + proj C x proj F x proj A x + proj C x + proj F x
89 66 69 88 syl2anc x proj A x + proj C x + proj F x
90 hvaddcl proj B x + proj D x proj G x proj B x + proj D x + proj G x
91 68 70 90 syl2anc x proj B x + proj D x + proj G x
92 hvpncan2 proj A x + proj C x + proj F x proj B x + proj D x + proj G x proj A x + proj C x + proj F x + proj B x + proj D x + proj G x - proj A x + proj C x + proj F x = proj B x + proj D x + proj G x
93 89 91 92 syl2anc x proj A x + proj C x + proj F x + proj B x + proj D x + proj G x - proj A x + proj C x + proj F x = proj B x + proj D x + proj G x
94 22 93 syl x X Y proj A x + proj C x + proj F x + proj B x + proj D x + proj G x - proj A x + proj C x + proj F x = proj B x + proj D x + proj G x
95 87 94 eqtr3d x X Y 2 x = proj B x + proj D x + proj G x
96 2 pjcli x proj B x B
97 4 pjcli x proj D x D
98 2 chshii B S
99 4 chshii D S
100 98 99 shsvai proj B x B proj D x D proj B x + proj D x B + D
101 96 97 100 syl2anc x proj B x + proj D x B + D
102 6 pjcli x proj G x G
103 98 99 shscli B + D S
104 6 chshii G S
105 103 104 shsvai proj B x + proj D x B + D proj G x G proj B x + proj D x + proj G x B + D + G
106 101 102 105 syl2anc x proj B x + proj D x + proj G x B + D + G
107 22 106 syl x X Y proj B x + proj D x + proj G x B + D + G
108 95 107 eqeltrd x X Y 2 x B + D + G
109 103 104 shscli B + D + G S
110 shmulcl B + D + G S 1 2 2 x B + D + G 1 2 2 x B + D + G
111 109 29 110 mp3an12 2 x B + D + G 1 2 2 x B + D + G
112 108 111 syl x X Y 1 2 2 x B + D + G
113 34 112 eqeltrd x X Y x B + D + G
114 113 ssriv X Y B + D + G
115 2 4 chsleji B + D B D
116 2 4 chjcli B D C
117 116 chshii B D S
118 103 117 104 shlessi B + D B D B + D + G B D + G
119 115 118 ax-mp B + D + G B D + G
120 114 119 sstri X Y B D + G
121 116 6 chsleji B D + G B D G
122 120 121 sstri X Y B D G
123 122 15 sseqtrri X Y Z