# 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 )`
` |-  ( ( ( 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 ) )`