Metamath Proof Explorer

Theorem chscllem4

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 ) ) )
chscl.7 
|- G = ( n e. NN |-> ( ( projh ` B ) ` ( H ` n ) ) )
Assertion chscllem4 
|- ( ph -> u e. ( A +H B ) )

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 chscl.7 
 |-  G = ( n e. NN |-> ( ( projh ` B ) ` ( H ` n ) ) )
8 hlimf 
 |-  ~~>v : dom ~~>v --> ~H
9 ffun 
 |-  ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v )
10 8 9 ax-mp 
 |-  Fun ~~>v
11 funbrfv 
 |-  ( Fun ~~>v -> ( H ~~>v u -> ( ~~>v ` H ) = u ) )
12 10 5 11 mpsyl 
 |-  ( ph -> ( ~~>v ` H ) = u )
13 4 feqmptd 
 |-  ( ph -> H = ( k e. NN |-> ( H ` k ) ) )
14 4 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( H ` k ) e. ( A +H B ) )
15 chsh 
 |-  ( A e. CH -> A e. SH )
16 1 15 syl 
 |-  ( ph -> A e. SH )
17 chsh 
 |-  ( B e. CH -> B e. SH )
18 2 17 syl 
 |-  ( ph -> B e. SH )
19 shsel 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( H ` k ) e. ( A +H B ) <-> E. x e. A E. y e. B ( H ` k ) = ( x +h y ) ) )
20 16 18 19 syl2anc 
 |-  ( ph -> ( ( H ` k ) e. ( A +H B ) <-> E. x e. A E. y e. B ( H ` k ) = ( x +h y ) ) )
21 20 biimpa 
 |-  ( ( ph /\ ( H ` k ) e. ( A +H B ) ) -> E. x e. A E. y e. B ( H ` k ) = ( x +h y ) )
22 14 21 syldan 
 |-  ( ( ph /\ k e. NN ) -> E. x e. A E. y e. B ( H ` k ) = ( x +h y ) )
23 simp3 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ( H ` k ) = ( x +h y ) )
24 simp1l 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ph )
25 24 1 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> A e. CH )
26 24 2 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> B e. CH )
27 24 3 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> B C_ ( _|_ ` A ) )
28 24 4 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> H : NN --> ( A +H B ) )
29 24 5 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> H ~~>v u )
30 simp1r 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> k e. NN )
31 simp2l 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> x e. A )
32 simp2r 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> y e. B )
33 25 26 27 28 29 6 30 31 32 23 chscllem3 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> x = ( F ` k ) )
34 chsscon2 
 |-  ( ( B e. CH /\ A e. CH ) -> ( B C_ ( _|_ ` A ) <-> A C_ ( _|_ ` B ) ) )
35 2 1 34 syl2anc 
 |-  ( ph -> ( B C_ ( _|_ ` A ) <-> A C_ ( _|_ ` B ) ) )
36 3 35 mpbid 
 |-  ( ph -> A C_ ( _|_ ` B ) )
37 24 36 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> A C_ ( _|_ ` B ) )
38 shscom 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
39 16 18 38 syl2anc 
 |-  ( ph -> ( A +H B ) = ( B +H A ) )
40 39 feq3d 
 |-  ( ph -> ( H : NN --> ( A +H B ) <-> H : NN --> ( B +H A ) ) )
41 4 40 mpbid 
 |-  ( ph -> H : NN --> ( B +H A ) )
42 24 41 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> H : NN --> ( B +H A ) )
43 shss 
 |-  ( A e. SH -> A C_ ~H )
44 16 43 syl 
 |-  ( ph -> A C_ ~H )
45 24 44 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> A C_ ~H )
46 45 31 sseldd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> x e. ~H )
47 shss 
 |-  ( B e. SH -> B C_ ~H )
48 18 47 syl 
 |-  ( ph -> B C_ ~H )
49 24 48 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> B C_ ~H )
50 49 32 sseldd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> y e. ~H )
51 ax-hvcom 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) = ( y +h x ) )
52 46 50 51 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ( x +h y ) = ( y +h x ) )
53 23 52 eqtrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ( H ` k ) = ( y +h x ) )
54 26 25 37 42 29 7 30 32 31 53 chscllem3 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> y = ( G ` k ) )
55 33 54 oveq12d 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ( x +h y ) = ( ( F ` k ) +h ( G ` k ) ) )
56 23 55 eqtrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( x e. A /\ y e. B ) /\ ( H ` k ) = ( x +h y ) ) -> ( H ` k ) = ( ( F ` k ) +h ( G ` k ) ) )
57 56 3exp 
 |-  ( ( ph /\ k e. NN ) -> ( ( x e. A /\ y e. B ) -> ( ( H ` k ) = ( x +h y ) -> ( H ` k ) = ( ( F ` k ) +h ( G ` k ) ) ) ) )
58 57 rexlimdvv 
 |-  ( ( ph /\ k e. NN ) -> ( E. x e. A E. y e. B ( H ` k ) = ( x +h y ) -> ( H ` k ) = ( ( F ` k ) +h ( G ` k ) ) ) )
59 22 58 mpd 
 |-  ( ( ph /\ k e. NN ) -> ( H ` k ) = ( ( F ` k ) +h ( G ` k ) ) )
60 59 mpteq2dva 
 |-  ( ph -> ( k e. NN |-> ( H ` k ) ) = ( k e. NN |-> ( ( F ` k ) +h ( G ` k ) ) ) )
61 13 60 eqtrd 
 |-  ( ph -> H = ( k e. NN |-> ( ( F ` k ) +h ( G ` k ) ) ) )
62 1 2 3 4 5 6 chscllem1 
 |-  ( ph -> F : NN --> A )
63 62 44 fssd 
 |-  ( ph -> F : NN --> ~H )
64 2 1 36 41 5 7 chscllem1 
 |-  ( ph -> G : NN --> B )
65 64 48 fssd 
 |-  ( ph -> G : NN --> ~H )
66 1 2 3 4 5 6 chscllem2 
 |-  ( ph -> F e. dom ~~>v )
67 funfvbrb 
 |-  ( Fun ~~>v -> ( F e. dom ~~>v <-> F ~~>v ( ~~>v ` F ) ) )
68 10 67 ax-mp 
 |-  ( F e. dom ~~>v <-> F ~~>v ( ~~>v ` F ) )
69 66 68 sylib 
 |-  ( ph -> F ~~>v ( ~~>v ` F ) )
70 2 1 36 41 5 7 chscllem2 
 |-  ( ph -> G e. dom ~~>v )
71 funfvbrb 
 |-  ( Fun ~~>v -> ( G e. dom ~~>v <-> G ~~>v ( ~~>v ` G ) ) )
72 10 71 ax-mp 
 |-  ( G e. dom ~~>v <-> G ~~>v ( ~~>v ` G ) )
73 70 72 sylib 
 |-  ( ph -> G ~~>v ( ~~>v ` G ) )
74 eqid 
 |-  ( k e. NN |-> ( ( F ` k ) +h ( G ` k ) ) ) = ( k e. NN |-> ( ( F ` k ) +h ( G ` k ) ) )
75 63 65 69 73 74 hlimadd 
 |-  ( ph -> ( k e. NN |-> ( ( F ` k ) +h ( G ` k ) ) ) ~~>v ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) )
76 61 75 eqbrtrd 
 |-  ( ph -> H ~~>v ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) )
77 funbrfv 
 |-  ( Fun ~~>v -> ( H ~~>v ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) -> ( ~~>v ` H ) = ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) ) )
78 10 76 77 mpsyl 
 |-  ( ph -> ( ~~>v ` H ) = ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) )
79 12 78 eqtr3d 
 |-  ( ph -> u = ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) )
80 fvex 
 |-  ( ~~>v ` F ) e. _V
81 80 chlimi 
 |-  ( ( A e. CH /\ F : NN --> A /\ F ~~>v ( ~~>v ` F ) ) -> ( ~~>v ` F ) e. A )
82 1 62 69 81 syl3anc 
 |-  ( ph -> ( ~~>v ` F ) e. A )
83 fvex 
 |-  ( ~~>v ` G ) e. _V
84 83 chlimi 
 |-  ( ( B e. CH /\ G : NN --> B /\ G ~~>v ( ~~>v ` G ) ) -> ( ~~>v ` G ) e. B )
85 2 64 73 84 syl3anc 
 |-  ( ph -> ( ~~>v ` G ) e. B )
86 shsva 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( ( ~~>v ` F ) e. A /\ ( ~~>v ` G ) e. B ) -> ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) e. ( A +H B ) ) )
87 16 18 86 syl2anc 
 |-  ( ph -> ( ( ( ~~>v ` F ) e. A /\ ( ~~>v ` G ) e. B ) -> ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) e. ( A +H B ) ) )
88 82 85 87 mp2and 
 |-  ( ph -> ( ( ~~>v ` F ) +h ( ~~>v ` G ) ) e. ( A +H B ) )
89 79 88 eqeltrd 
 |-  ( ph -> u e. ( A +H B ) )