Metamath Proof Explorer

Theorem shuni

Description: Two subspaces with trivial intersection have a unique decomposition of the elements of the subspace sum. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses shuni.1 
|- ( ph -> H e. SH )
shuni.2 
|- ( ph -> K e. SH )
shuni.3 
|- ( ph -> ( H i^i K ) = 0H )
shuni.4 
|- ( ph -> A e. H )
shuni.5 
|- ( ph -> B e. K )
shuni.6 
|- ( ph -> C e. H )
shuni.7 
|- ( ph -> D e. K )
shuni.8 
|- ( ph -> ( A +h B ) = ( C +h D ) )
Assertion shuni 
|- ( ph -> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 shuni.1 
 |-  ( ph -> H e. SH )
2 shuni.2 
 |-  ( ph -> K e. SH )
3 shuni.3 
 |-  ( ph -> ( H i^i K ) = 0H )
4 shuni.4 
 |-  ( ph -> A e. H )
5 shuni.5 
 |-  ( ph -> B e. K )
6 shuni.6 
 |-  ( ph -> C e. H )
7 shuni.7 
 |-  ( ph -> D e. K )
8 shuni.8 
 |-  ( ph -> ( A +h B ) = ( C +h D ) )
9 shsubcl 
 |-  ( ( H e. SH /\ A e. H /\ C e. H ) -> ( A -h C ) e. H )
10 1 4 6 9 syl3anc 
 |-  ( ph -> ( A -h C ) e. H )
11 shel 
 |-  ( ( H e. SH /\ A e. H ) -> A e. ~H )
12 1 4 11 syl2anc 
 |-  ( ph -> A e. ~H )
13 shel 
 |-  ( ( K e. SH /\ B e. K ) -> B e. ~H )
14 2 5 13 syl2anc 
 |-  ( ph -> B e. ~H )
15 shel 
 |-  ( ( H e. SH /\ C e. H ) -> C e. ~H )
16 1 6 15 syl2anc 
 |-  ( ph -> C e. ~H )
17 shel 
 |-  ( ( K e. SH /\ D e. K ) -> D e. ~H )
18 2 7 17 syl2anc 
 |-  ( ph -> D e. ~H )
19 hvaddsub4 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) = ( C +h D ) <-> ( A -h C ) = ( D -h B ) ) )
20 12 14 16 18 19 syl22anc 
 |-  ( ph -> ( ( A +h B ) = ( C +h D ) <-> ( A -h C ) = ( D -h B ) ) )
21 8 20 mpbid 
 |-  ( ph -> ( A -h C ) = ( D -h B ) )
22 shsubcl 
 |-  ( ( K e. SH /\ D e. K /\ B e. K ) -> ( D -h B ) e. K )
23 2 7 5 22 syl3anc 
 |-  ( ph -> ( D -h B ) e. K )
24 21 23 eqeltrd 
 |-  ( ph -> ( A -h C ) e. K )
25 10 24 elind 
 |-  ( ph -> ( A -h C ) e. ( H i^i K ) )
26 25 3 eleqtrd 
 |-  ( ph -> ( A -h C ) e. 0H )
27 elch0 
 |-  ( ( A -h C ) e. 0H <-> ( A -h C ) = 0h )
28 26 27 sylib 
 |-  ( ph -> ( A -h C ) = 0h )
29 hvsubeq0 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( ( A -h C ) = 0h <-> A = C ) )
30 12 16 29 syl2anc 
 |-  ( ph -> ( ( A -h C ) = 0h <-> A = C ) )
31 28 30 mpbid 
 |-  ( ph -> A = C )
32 21 28 eqtr3d 
 |-  ( ph -> ( D -h B ) = 0h )
33 hvsubeq0 
 |-  ( ( D e. ~H /\ B e. ~H ) -> ( ( D -h B ) = 0h <-> D = B ) )
34 18 14 33 syl2anc 
 |-  ( ph -> ( ( D -h B ) = 0h <-> D = B ) )
35 32 34 mpbid 
 |-  ( ph -> D = B )
36 35 eqcomd 
 |-  ( ph -> B = D )
37 31 36 jca 
 |-  ( ph -> ( A = C /\ B = D ) )