Metamath Proof Explorer

Theorem pjjsi

Description: A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjjs.1 
|- G e. CH
pjjs.2 
|- H e. SH
Assertion pjjsi 
|- ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( G vH H ) = ( G +H H ) )

Proof

Step Hyp Ref Expression
1 pjjs.1 
 |-  G e. CH
2 pjjs.2 
 |-  H e. SH
3 fveq2 
 |-  ( x = w -> ( ( projh ` ( _|_ ` G ) ) ` x ) = ( ( projh ` ( _|_ ` G ) ) ` w ) )
4 3 eleq1d 
 |-  ( x = w -> ( ( ( projh ` ( _|_ ` G ) ) ` x ) e. H <-> ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) )
5 4 rspcv 
 |-  ( w e. ( G vH H ) -> ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) )
6 1 chshii 
 |-  G e. SH
7 6 2 shjcli 
 |-  ( G vH H ) e. CH
8 7 cheli 
 |-  ( w e. ( G vH H ) -> w e. ~H )
9 1 pjcli 
 |-  ( w e. ~H -> ( ( projh ` G ) ` w ) e. G )
10 9 anim1i 
 |-  ( ( w e. ~H /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> ( ( ( projh ` G ) ` w ) e. G /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) )
11 axpjpj 
 |-  ( ( G e. CH /\ w e. ~H ) -> w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) )
12 1 11 mpan 
 |-  ( w e. ~H -> w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) )
13 12 adantr 
 |-  ( ( w e. ~H /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) )
14 10 13 jca 
 |-  ( ( w e. ~H /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> ( ( ( ( projh ` G ) ` w ) e. G /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) /\ w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) ) )
15 8 14 sylan 
 |-  ( ( w e. ( G vH H ) /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> ( ( ( ( projh ` G ) ` w ) e. G /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) /\ w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) ) )
16 rspceov 
 |-  ( ( ( ( projh ` G ) ` w ) e. G /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H /\ w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) ) -> E. y e. G E. z e. H w = ( y +h z ) )
17 16 3expa 
 |-  ( ( ( ( ( projh ` G ) ` w ) e. G /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) /\ w = ( ( ( projh ` G ) ` w ) +h ( ( projh ` ( _|_ ` G ) ) ` w ) ) ) -> E. y e. G E. z e. H w = ( y +h z ) )
18 15 17 syl 
 |-  ( ( w e. ( G vH H ) /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> E. y e. G E. z e. H w = ( y +h z ) )
19 6 2 shseli 
 |-  ( w e. ( G +H H ) <-> E. y e. G E. z e. H w = ( y +h z ) )
20 18 19 sylibr 
 |-  ( ( w e. ( G vH H ) /\ ( ( projh ` ( _|_ ` G ) ) ` w ) e. H ) -> w e. ( G +H H ) )
21 20 ex 
 |-  ( w e. ( G vH H ) -> ( ( ( projh ` ( _|_ ` G ) ) ` w ) e. H -> w e. ( G +H H ) ) )
22 5 21 syldc 
 |-  ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( w e. ( G vH H ) -> w e. ( G +H H ) ) )
23 22 ssrdv 
 |-  ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( G vH H ) C_ ( G +H H ) )
24 6 2 shsleji 
 |-  ( G +H H ) C_ ( G vH H )
25 23 24 jctir 
 |-  ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( ( G vH H ) C_ ( G +H H ) /\ ( G +H H ) C_ ( G vH H ) ) )
26 eqss 
 |-  ( ( G vH H ) = ( G +H H ) <-> ( ( G vH H ) C_ ( G +H H ) /\ ( G +H H ) C_ ( G vH H ) ) )
27 25 26 sylibr 
 |-  ( A. x e. ( G vH H ) ( ( projh ` ( _|_ ` G ) ) ` x ) e. H -> ( G vH H ) = ( G +H H ) )