Step |
Hyp |
Ref |
Expression |
1 |
|
chscl.1 |
|- ( ph -> A e. CH ) |
2 |
|
chscl.2 |
|- ( ph -> B e. CH ) |
3 |
|
chscl.3 |
|- ( ph -> B C_ ( _|_ ` A ) ) |
4 |
|
chsh |
|- ( A e. CH -> A e. SH ) |
5 |
1 4
|
syl |
|- ( ph -> A e. SH ) |
6 |
|
chsh |
|- ( B e. CH -> B e. SH ) |
7 |
2 6
|
syl |
|- ( ph -> B e. SH ) |
8 |
|
shscl |
|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) e. SH ) |
9 |
5 7 8
|
syl2anc |
|- ( ph -> ( A +H B ) e. SH ) |
10 |
1
|
adantr |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> A e. CH ) |
11 |
2
|
adantr |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> B e. CH ) |
12 |
3
|
adantr |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> B C_ ( _|_ ` A ) ) |
13 |
|
simprl |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> f : NN --> ( A +H B ) ) |
14 |
|
simprr |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> f ~~>v z ) |
15 |
|
eqid |
|- ( x e. NN |-> ( ( projh ` A ) ` ( f ` x ) ) ) = ( x e. NN |-> ( ( projh ` A ) ` ( f ` x ) ) ) |
16 |
|
eqid |
|- ( x e. NN |-> ( ( projh ` B ) ` ( f ` x ) ) ) = ( x e. NN |-> ( ( projh ` B ) ` ( f ` x ) ) ) |
17 |
10 11 12 13 14 15 16
|
chscllem4 |
|- ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> z e. ( A +H B ) ) |
18 |
17
|
ex |
|- ( ph -> ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) ) |
19 |
18
|
alrimivv |
|- ( ph -> A. f A. z ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) ) |
20 |
|
isch2 |
|- ( ( A +H B ) e. CH <-> ( ( A +H B ) e. SH /\ A. f A. z ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) ) ) |
21 |
9 19 20
|
sylanbrc |
|- ( ph -> ( A +H B ) e. CH ) |