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 ) ) ) ) ) ) |