Metamath Proof Explorer

Theorem chscllem1

Description: Lemma for chscl . (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1 
|- ( ph -> A e. CH )
chscl.2 
|- ( ph -> B e. CH )
chscl.3 
|- ( ph -> B C_ ( _|_ ` A ) )
chscl.4 
|- ( ph -> H : NN --> ( A +H B ) )
chscl.5 
|- ( ph -> H ~~>v u )
chscl.6 
|- F = ( n e. NN |-> ( ( projh ` A ) ` ( H ` n ) ) )
Assertion chscllem1 
|- ( ph -> F : NN --> A )

Proof

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 chscl.4 
 |-  ( ph -> H : NN --> ( A +H B ) )
5 chscl.5 
 |-  ( ph -> H ~~>v u )
6 chscl.6 
 |-  F = ( n e. NN |-> ( ( projh ` A ) ` ( H ` n ) ) )
7 eqid 
 |-  ( ( projh ` A ) ` ( H ` n ) ) = ( ( projh ` A ) ` ( H ` n ) )
8 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. CH )
9 4 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( H ` n ) e. ( A +H B ) )
10 chsh 
 |-  ( B e. CH -> B e. SH )
11 2 10 syl 
 |-  ( ph -> B e. SH )
12 chsh 
 |-  ( A e. CH -> A e. SH )
13 1 12 syl 
 |-  ( ph -> A e. SH )
14 shocsh 
 |-  ( A e. SH -> ( _|_ ` A ) e. SH )
15 13 14 syl 
 |-  ( ph -> ( _|_ ` A ) e. SH )
16 shless 
 |-  ( ( ( B e. SH /\ ( _|_ ` A ) e. SH /\ A e. SH ) /\ B C_ ( _|_ ` A ) ) -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
17 11 15 13 3 16 syl31anc 
 |-  ( ph -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
18 shscom 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
19 13 11 18 syl2anc 
 |-  ( ph -> ( A +H B ) = ( B +H A ) )
20 shscom 
 |-  ( ( A e. SH /\ ( _|_ ` A ) e. SH ) -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
21 13 15 20 syl2anc 
 |-  ( ph -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
22 17 19 21 3sstr4d 
 |-  ( ph -> ( A +H B ) C_ ( A +H ( _|_ ` A ) ) )
23 22 sselda 
 |-  ( ( ph /\ ( H ` n ) e. ( A +H B ) ) -> ( H ` n ) e. ( A +H ( _|_ ` A ) ) )
24 9 23 syldan 
 |-  ( ( ph /\ n e. NN ) -> ( H ` n ) e. ( A +H ( _|_ ` A ) ) )
25 pjpreeq 
 |-  ( ( A e. CH /\ ( H ` n ) e. ( A +H ( _|_ ` A ) ) ) -> ( ( ( projh ` A ) ` ( H ` n ) ) = ( ( projh ` A ) ` ( H ` n ) ) <-> ( ( ( projh ` A ) ` ( H ` n ) ) e. A /\ E. x e. ( _|_ ` A ) ( H ` n ) = ( ( ( projh ` A ) ` ( H ` n ) ) +h x ) ) ) )
26 8 24 25 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( projh ` A ) ` ( H ` n ) ) = ( ( projh ` A ) ` ( H ` n ) ) <-> ( ( ( projh ` A ) ` ( H ` n ) ) e. A /\ E. x e. ( _|_ ` A ) ( H ` n ) = ( ( ( projh ` A ) ` ( H ` n ) ) +h x ) ) ) )
27 7 26 mpbii 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( projh ` A ) ` ( H ` n ) ) e. A /\ E. x e. ( _|_ ` A ) ( H ` n ) = ( ( ( projh ` A ) ` ( H ` n ) ) +h x ) ) )
28 27 simpld 
 |-  ( ( ph /\ n e. NN ) -> ( ( projh ` A ) ` ( H ` n ) ) e. A )
29 28 6 fmptd 
 |-  ( ph -> F : NN --> A )