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 e. CH
mayete3.b 
|- B e. CH
mayete3.c 
|- C e. CH
mayete3.d 
|- D e. CH
mayete3.f 
|- F e. CH
mayete3.g 
|- G e. CH
mayete3.ac 
|- A C_ ( _|_ ` C )
mayete3.af 
|- A C_ ( _|_ ` F )
mayete3.cf 
|- C C_ ( _|_ ` F )
mayete3.ab 
|- A C_ ( _|_ ` B )
mayete3.cd 
|- C C_ ( _|_ ` D )
mayete3.fg 
|- F C_ ( _|_ ` G )
mayete3.x 
|- X = ( ( A vH C ) vH F )
mayete3.y 
|- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )
mayete3.z 
|- Z = ( ( B vH D ) vH G )
Assertion mayete3i 
|- ( X i^i Y ) C_ Z

Proof

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