Metamath Proof Explorer

Theorem chscllem3

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 ) ) )
chscllem3.7 
|- ( ph -> N e. NN )
chscllem3.8 
|- ( ph -> C e. A )
chscllem3.9 
|- ( ph -> D e. B )
chscllem3.10 
|- ( ph -> ( H ` N ) = ( C +h D ) )
Assertion chscllem3 
|- ( ph -> C = ( F ` N ) )

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 chscllem3.7 
 |-  ( ph -> N e. NN )
8 chscllem3.8 
 |-  ( ph -> C e. A )
9 chscllem3.9 
 |-  ( ph -> D e. B )
10 chscllem3.10 
 |-  ( ph -> ( H ` N ) = ( C +h D ) )
11 2fveq3 
 |-  ( n = N -> ( ( projh ` A ) ` ( H ` n ) ) = ( ( projh ` A ) ` ( H ` N ) ) )
12 fvex 
 |-  ( ( projh ` A ) ` ( H ` N ) ) e. _V
13 11 6 12 fvmpt 
 |-  ( N e. NN -> ( F ` N ) = ( ( projh ` A ) ` ( H ` N ) ) )
14 7 13 syl 
 |-  ( ph -> ( F ` N ) = ( ( projh ` A ) ` ( H ` N ) ) )
15 14 eqcomd 
 |-  ( ph -> ( ( projh ` A ) ` ( H ` N ) ) = ( F ` N ) )
16 chsh 
 |-  ( B e. CH -> B e. SH )
17 2 16 syl 
 |-  ( ph -> B e. SH )
18 chsh 
 |-  ( A e. CH -> A e. SH )
19 1 18 syl 
 |-  ( ph -> A e. SH )
20 shocsh 
 |-  ( A e. SH -> ( _|_ ` A ) e. SH )
21 19 20 syl 
 |-  ( ph -> ( _|_ ` A ) e. SH )
22 shless 
 |-  ( ( ( B e. SH /\ ( _|_ ` A ) e. SH /\ A e. SH ) /\ B C_ ( _|_ ` A ) ) -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
23 17 21 19 3 22 syl31anc 
 |-  ( ph -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
24 shscom 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
25 19 17 24 syl2anc 
 |-  ( ph -> ( A +H B ) = ( B +H A ) )
26 shscom 
 |-  ( ( A e. SH /\ ( _|_ ` A ) e. SH ) -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
27 19 21 26 syl2anc 
 |-  ( ph -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
28 23 25 27 3sstr4d 
 |-  ( ph -> ( A +H B ) C_ ( A +H ( _|_ ` A ) ) )
29 4 7 ffvelrnd 
 |-  ( ph -> ( H ` N ) e. ( A +H B ) )
30 28 29 sseldd 
 |-  ( ph -> ( H ` N ) e. ( A +H ( _|_ ` A ) ) )
31 pjpreeq 
 |-  ( ( A e. CH /\ ( H ` N ) e. ( A +H ( _|_ ` A ) ) ) -> ( ( ( projh ` A ) ` ( H ` N ) ) = ( F ` N ) <-> ( ( F ` N ) e. A /\ E. z e. ( _|_ ` A ) ( H ` N ) = ( ( F ` N ) +h z ) ) ) )
32 1 30 31 syl2anc 
 |-  ( ph -> ( ( ( projh ` A ) ` ( H ` N ) ) = ( F ` N ) <-> ( ( F ` N ) e. A /\ E. z e. ( _|_ ` A ) ( H ` N ) = ( ( F ` N ) +h z ) ) ) )
33 15 32 mpbid 
 |-  ( ph -> ( ( F ` N ) e. A /\ E. z e. ( _|_ ` A ) ( H ` N ) = ( ( F ` N ) +h z ) ) )
34 33 simprd 
 |-  ( ph -> E. z e. ( _|_ ` A ) ( H ` N ) = ( ( F ` N ) +h z ) )
35 19 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> A e. SH )
36 21 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( _|_ ` A ) e. SH )
37 ocin 
 |-  ( A e. SH -> ( A i^i ( _|_ ` A ) ) = 0H )
38 19 37 syl 
 |-  ( ph -> ( A i^i ( _|_ ` A ) ) = 0H )
39 38 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( A i^i ( _|_ ` A ) ) = 0H )
40 8 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> C e. A )
41 3 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> B C_ ( _|_ ` A ) )
42 9 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> D e. B )
43 41 42 sseldd 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> D e. ( _|_ ` A ) )
44 1 2 3 4 5 6 chscllem1 
 |-  ( ph -> F : NN --> A )
45 44 7 ffvelrnd 
 |-  ( ph -> ( F ` N ) e. A )
46 45 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( F ` N ) e. A )
47 simprl 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> z e. ( _|_ ` A ) )
48 10 adantr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( H ` N ) = ( C +h D ) )
49 simprr 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( H ` N ) = ( ( F ` N ) +h z ) )
50 48 49 eqtr3d 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( C +h D ) = ( ( F ` N ) +h z ) )
51 35 36 39 40 43 46 47 50 shuni 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> ( C = ( F ` N ) /\ D = z ) )
52 51 simpld 
 |-  ( ( ph /\ ( z e. ( _|_ ` A ) /\ ( H ` N ) = ( ( F ` N ) +h z ) ) ) -> C = ( F ` N ) )
53 34 52 rexlimddv 
 |-  ( ph -> C = ( F ` N ) )