Metamath Proof Explorer

Theorem mayetes3i

Description: Mayet's equation E^*_3, derived from E_3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of Mayet3 p. 1240. (Contributed by NM, 10-May-2009) (New usage is discouraged.)

Ref Expression
Hypotheses mayetes3.a 
|- A e. CH
mayetes3.b 
|- B e. CH
mayetes3.c 
|- C e. CH
mayetes3.d 
|- D e. CH
mayetes3.f 
|- F e. CH
mayetes3.g 
|- G e. CH
mayetes3.r 
|- R e. CH
mayetes3.ac 
|- A C_ ( _|_ ` C )
mayetes3.af 
|- A C_ ( _|_ ` F )
mayetes3.cf 
|- C C_ ( _|_ ` F )
mayetes3.ab 
|- A C_ ( _|_ ` B )
mayetes3.cd 
|- C C_ ( _|_ ` D )
mayetes3.fg 
|- F C_ ( _|_ ` G )
mayetes3.rx 
|- R C_ ( _|_ ` X )
mayetes3.x 
|- X = ( ( A vH C ) vH F )
mayetes3.y 
|- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )
mayetes3.z 
|- Z = ( ( B vH D ) vH G )
Assertion mayetes3i 
|- ( ( X vH R ) i^i Y ) C_ ( Z vH R )

Proof

Step Hyp Ref Expression
1 mayetes3.a 
 |-  A e. CH
2 mayetes3.b 
 |-  B e. CH
3 mayetes3.c 
 |-  C e. CH
4 mayetes3.d 
 |-  D e. CH
5 mayetes3.f 
 |-  F e. CH
6 mayetes3.g 
 |-  G e. CH
7 mayetes3.r 
 |-  R e. CH
8 mayetes3.ac 
 |-  A C_ ( _|_ ` C )
9 mayetes3.af 
 |-  A C_ ( _|_ ` F )
10 mayetes3.cf 
 |-  C C_ ( _|_ ` F )
11 mayetes3.ab 
 |-  A C_ ( _|_ ` B )
12 mayetes3.cd 
 |-  C C_ ( _|_ ` D )
13 mayetes3.fg 
 |-  F C_ ( _|_ ` G )
14 mayetes3.rx 
 |-  R C_ ( _|_ ` X )
15 mayetes3.x 
 |-  X = ( ( A vH C ) vH F )
16 mayetes3.y 
 |-  Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )
17 mayetes3.z 
 |-  Z = ( ( B vH D ) vH G )
18 1 3 chjcli 
 |-  ( A vH C ) e. CH
19 18 5 chjcli 
 |-  ( ( A vH C ) vH F ) e. CH
20 19 7 chjcomi 
 |-  ( ( ( A vH C ) vH F ) vH R ) = ( R vH ( ( A vH C ) vH F ) )
21 20 eqimssi 
 |-  ( ( ( A vH C ) vH F ) vH R ) C_ ( R vH ( ( A vH C ) vH F ) )
22 1 2 chjcli 
 |-  ( A vH B ) e. CH
23 22 7 chub1i 
 |-  ( A vH B ) C_ ( ( A vH B ) vH R )
24 1 2 7 chjassi 
 |-  ( ( A vH B ) vH R ) = ( A vH ( B vH R ) )
25 23 24 sseqtri 
 |-  ( A vH B ) C_ ( A vH ( B vH R ) )
26 2 7 chjcli 
 |-  ( B vH R ) e. CH
27 1 26 chjcli 
 |-  ( A vH ( B vH R ) ) e. CH
28 27 7 chub2i 
 |-  ( A vH ( B vH R ) ) C_ ( R vH ( A vH ( B vH R ) ) )
29 25 28 sstri 
 |-  ( A vH B ) C_ ( R vH ( A vH ( B vH R ) ) )
30 3 4 chjcli 
 |-  ( C vH D ) e. CH
31 30 7 chub1i 
 |-  ( C vH D ) C_ ( ( C vH D ) vH R )
32 3 4 7 chjassi 
 |-  ( ( C vH D ) vH R ) = ( C vH ( D vH R ) )
33 31 32 sseqtri 
 |-  ( C vH D ) C_ ( C vH ( D vH R ) )
34 4 7 chjcli 
 |-  ( D vH R ) e. CH
35 3 34 chjcli 
 |-  ( C vH ( D vH R ) ) e. CH
36 35 7 chub2i 
 |-  ( C vH ( D vH R ) ) C_ ( R vH ( C vH ( D vH R ) ) )
37 33 36 sstri 
 |-  ( C vH D ) C_ ( R vH ( C vH ( D vH R ) ) )
38 ss2in 
 |-  ( ( ( A vH B ) C_ ( R vH ( A vH ( B vH R ) ) ) /\ ( C vH D ) C_ ( R vH ( C vH ( D vH R ) ) ) ) -> ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) )
39 29 37 38 mp2an 
 |-  ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) )
40 5 6 chjcli 
 |-  ( F vH G ) e. CH
41 40 7 chub1i 
 |-  ( F vH G ) C_ ( ( F vH G ) vH R )
42 5 6 7 chjassi 
 |-  ( ( F vH G ) vH R ) = ( F vH ( G vH R ) )
43 41 42 sseqtri 
 |-  ( F vH G ) C_ ( F vH ( G vH R ) )
44 6 7 chjcli 
 |-  ( G vH R ) e. CH
45 5 44 chjcli 
 |-  ( F vH ( G vH R ) ) e. CH
46 45 7 chub2i 
 |-  ( F vH ( G vH R ) ) C_ ( R vH ( F vH ( G vH R ) ) )
47 43 46 sstri 
 |-  ( F vH G ) C_ ( R vH ( F vH ( G vH R ) ) )
48 ss2in 
 |-  ( ( ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) /\ ( F vH G ) C_ ( R vH ( F vH ( G vH R ) ) ) ) -> ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
49 39 47 48 mp2an 
 |-  ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
50 ss2in 
 |-  ( ( ( ( ( A vH C ) vH F ) vH R ) C_ ( R vH ( ( A vH C ) vH F ) ) /\ ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) -> ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) )
51 21 49 50 mp2an 
 |-  ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
52 27 35 chincli 
 |-  ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) e. CH
53 52 45 chincli 
 |-  ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) e. CH
54 15 19 eqeltri 
 |-  X e. CH
55 54 choccli 
 |-  ( _|_ ` X ) e. CH
56 7 55 14 lecmii 
 |-  R C_H ( _|_ ` X )
57 7 54 cmcm2i 
 |-  ( R C_H X <-> R C_H ( _|_ ` X ) )
58 56 57 mpbir 
 |-  R C_H X
59 58 15 breqtri 
 |-  R C_H ( ( A vH C ) vH F )
60 7 2 chub2i 
 |-  R C_ ( B vH R )
61 26 1 chub2i 
 |-  ( B vH R ) C_ ( A vH ( B vH R ) )
62 60 61 sstri 
 |-  R C_ ( A vH ( B vH R ) )
63 7 27 62 lecmii 
 |-  R C_H ( A vH ( B vH R ) )
64 7 4 chub2i 
 |-  R C_ ( D vH R )
65 34 3 chub2i 
 |-  ( D vH R ) C_ ( C vH ( D vH R ) )
66 64 65 sstri 
 |-  R C_ ( C vH ( D vH R ) )
67 7 35 66 lecmii 
 |-  R C_H ( C vH ( D vH R ) )
68 7 27 35 63 67 cm2mi 
 |-  R C_H ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) )
69 7 6 chub2i 
 |-  R C_ ( G vH R )
70 44 5 chub2i 
 |-  ( G vH R ) C_ ( F vH ( G vH R ) )
71 69 70 sstri 
 |-  R C_ ( F vH ( G vH R ) )
72 7 45 71 lecmii 
 |-  R C_H ( F vH ( G vH R ) )
73 7 52 45 68 72 cm2mi 
 |-  R C_H ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) )
74 7 19 53 59 73 fh3i 
 |-  ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) = ( ( R vH ( ( A vH C ) vH F ) ) i^i ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
75 7 52 45 68 72 fh3i 
 |-  ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) = ( ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
76 7 27 35 63 67 fh3i 
 |-  ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) = ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) )
77 76 ineq1i 
 |-  ( ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) = ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
78 75 77 eqtri 
 |-  ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) = ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
79 78 ineq2i 
 |-  ( ( R vH ( ( A vH C ) vH F ) ) i^i ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) = ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
80 74 79 eqtr2i 
 |-  ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) = ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
81 51 80 sseqtri 
 |-  ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
82 2 4 chjcli 
 |-  ( B vH D ) e. CH
83 82 6 chjcli 
 |-  ( ( B vH D ) vH G ) e. CH
84 7 83 chub2i 
 |-  R C_ ( ( ( B vH D ) vH G ) vH R )
85 1 3 chub1i 
 |-  A C_ ( A vH C )
86 18 5 chub1i 
 |-  ( A vH C ) C_ ( ( A vH C ) vH F )
87 86 15 sseqtrri 
 |-  ( A vH C ) C_ X
88 85 87 sstri 
 |-  A C_ X
89 1 54 chsscon3i 
 |-  ( A C_ X <-> ( _|_ ` X ) C_ ( _|_ ` A ) )
90 88 89 mpbi 
 |-  ( _|_ ` X ) C_ ( _|_ ` A )
91 14 90 sstri 
 |-  R C_ ( _|_ ` A )
92 7 1 chsscon2i 
 |-  ( R C_ ( _|_ ` A ) <-> A C_ ( _|_ ` R ) )
93 91 92 mpbi 
 |-  A C_ ( _|_ ` R )
94 11 93 ssini 
 |-  A C_ ( ( _|_ ` B ) i^i ( _|_ ` R ) )
95 2 7 chdmj1i 
 |-  ( _|_ ` ( B vH R ) ) = ( ( _|_ ` B ) i^i ( _|_ ` R ) )
96 94 95 sseqtrri 
 |-  A C_ ( _|_ ` ( B vH R ) )
97 3 1 chub2i 
 |-  C C_ ( A vH C )
98 97 87 sstri 
 |-  C C_ X
99 3 54 chsscon3i 
 |-  ( C C_ X <-> ( _|_ ` X ) C_ ( _|_ ` C ) )
100 98 99 mpbi 
 |-  ( _|_ ` X ) C_ ( _|_ ` C )
101 14 100 sstri 
 |-  R C_ ( _|_ ` C )
102 7 3 chsscon2i 
 |-  ( R C_ ( _|_ ` C ) <-> C C_ ( _|_ ` R ) )
103 101 102 mpbi 
 |-  C C_ ( _|_ ` R )
104 12 103 ssini 
 |-  C C_ ( ( _|_ ` D ) i^i ( _|_ ` R ) )
105 4 7 chdmj1i 
 |-  ( _|_ ` ( D vH R ) ) = ( ( _|_ ` D ) i^i ( _|_ ` R ) )
106 104 105 sseqtrri 
 |-  C C_ ( _|_ ` ( D vH R ) )
107 5 18 chub2i 
 |-  F C_ ( ( A vH C ) vH F )
108 107 15 sseqtrri 
 |-  F C_ X
109 5 54 chsscon3i 
 |-  ( F C_ X <-> ( _|_ ` X ) C_ ( _|_ ` F ) )
110 108 109 mpbi 
 |-  ( _|_ ` X ) C_ ( _|_ ` F )
111 14 110 sstri 
 |-  R C_ ( _|_ ` F )
112 7 5 chsscon2i 
 |-  ( R C_ ( _|_ ` F ) <-> F C_ ( _|_ ` R ) )
113 111 112 mpbi 
 |-  F C_ ( _|_ ` R )
114 13 113 ssini 
 |-  F C_ ( ( _|_ ` G ) i^i ( _|_ ` R ) )
115 6 7 chdmj1i 
 |-  ( _|_ ` ( G vH R ) ) = ( ( _|_ ` G ) i^i ( _|_ ` R ) )
116 114 115 sseqtrri 
 |-  F C_ ( _|_ ` ( G vH R ) )
117 eqid 
 |-  ( ( A vH C ) vH F ) = ( ( A vH C ) vH F )
118 eqid 
 |-  ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) = ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) )
119 82 6 7 chjjdiri 
 |-  ( ( ( B vH D ) vH G ) vH R ) = ( ( ( B vH D ) vH R ) vH ( G vH R ) )
120 2 4 7 chjjdiri 
 |-  ( ( B vH D ) vH R ) = ( ( B vH R ) vH ( D vH R ) )
121 120 oveq1i 
 |-  ( ( ( B vH D ) vH R ) vH ( G vH R ) ) = ( ( ( B vH R ) vH ( D vH R ) ) vH ( G vH R ) )
122 119 121 eqtri 
 |-  ( ( ( B vH D ) vH G ) vH R ) = ( ( ( B vH R ) vH ( D vH R ) ) vH ( G vH R ) )
123 1 26 3 34 5 44 8 9 10 96 106 116 117 118 122 mayete3i 
 |-  ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
124 19 53 chincli 
 |-  ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) e. CH
125 83 7 chjcli 
 |-  ( ( ( B vH D ) vH G ) vH R ) e. CH
126 7 124 125 chlubii 
 |-  ( ( R C_ ( ( ( B vH D ) vH G ) vH R ) /\ ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R ) ) -> ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R ) )
127 84 123 126 mp2an 
 |-  ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
128 81 127 sstri 
 |-  ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
129 15 oveq1i 
 |-  ( X vH R ) = ( ( ( A vH C ) vH F ) vH R )
130 129 16 ineq12i 
 |-  ( ( X vH R ) i^i Y ) = ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) )
131 17 oveq1i 
 |-  ( Z vH R ) = ( ( ( B vH D ) vH G ) vH R )
132 128 130 131 3sstr4i 
 |-  ( ( X vH R ) i^i Y ) C_ ( Z vH R )