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 ⊢ ( 𝜑 → 𝐻 ∈ Sℋ )
shuni.2 ⊢ ( 𝜑 → 𝐾 ∈ Sℋ )
shuni.3 ⊢ ( 𝜑 → ( 𝐻 ∩ 𝐾 ) = 0ℋ )
shuni.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝐻 )
shuni.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
shuni.6 ⊢ ( 𝜑 → 𝐶 ∈ 𝐻 )
shuni.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝐾 )
shuni.8 ⊢ ( 𝜑 → ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) )
Assertion shuni ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 shuni.1 ⊢ ( 𝜑 → 𝐻 ∈ Sℋ )
2 shuni.2 ⊢ ( 𝜑 → 𝐾 ∈ Sℋ )
3 shuni.3 ⊢ ( 𝜑 → ( 𝐻 ∩ 𝐾 ) = 0ℋ )
4 shuni.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝐻 )
5 shuni.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
6 shuni.6 ⊢ ( 𝜑 → 𝐶 ∈ 𝐻 )
7 shuni.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝐾 )
8 shuni.8 ⊢ ( 𝜑 → ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) )
9 shsubcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐶 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐶 ) ∈ 𝐻 )
10 1 4 6 9 syl3anc ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) ∈ 𝐻 )
11 shel ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ) → 𝐴 ∈ ℋ )
12 1 4 11 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ ℋ )
13 shel ⊢ ( ( 𝐾 ∈ Sℋ ∧ 𝐵 ∈ 𝐾 ) → 𝐵 ∈ ℋ )
14 2 5 13 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ℋ )
15 shel ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐶 ∈ 𝐻 ) → 𝐶 ∈ ℋ )
16 1 6 15 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ ℋ )
17 shel ⊢ ( ( 𝐾 ∈ Sℋ ∧ 𝐷 ∈ 𝐾 ) → 𝐷 ∈ ℋ )
18 2 7 17 syl2anc ⊢ ( 𝜑 → 𝐷 ∈ ℋ )
19 hvaddsub4 ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) ↔ ( 𝐴 −ℎ 𝐶 ) = ( 𝐷 −ℎ 𝐵 ) ) )
20 12 14 16 18 19 syl22anc ⊢ ( 𝜑 → ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) ↔ ( 𝐴 −ℎ 𝐶 ) = ( 𝐷 −ℎ 𝐵 ) ) )
21 8 20 mpbid ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) = ( 𝐷 −ℎ 𝐵 ) )
22 shsubcl ⊢ ( ( 𝐾 ∈ Sℋ ∧ 𝐷 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐷 −ℎ 𝐵 ) ∈ 𝐾 )
23 2 7 5 22 syl3anc ⊢ ( 𝜑 → ( 𝐷 −ℎ 𝐵 ) ∈ 𝐾 )
24 21 23 eqeltrd ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) ∈ 𝐾 )
25 10 24 elind ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) ∈ ( 𝐻 ∩ 𝐾 ) )
26 25 3 eleqtrd ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) ∈ 0ℋ )
27 elch0 ⊢ ( ( 𝐴 −ℎ 𝐶 ) ∈ 0ℋ ↔ ( 𝐴 −ℎ 𝐶 ) = 0ℎ )
28 26 27 sylib ⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐶 ) = 0ℎ )
29 hvsubeq0 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐶 ) = 0ℎ ↔ 𝐴 = 𝐶 ) )
30 12 16 29 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐶 ) = 0ℎ ↔ 𝐴 = 𝐶 ) )
31 28 30 mpbid ⊢ ( 𝜑 → 𝐴 = 𝐶 )
32 21 28 eqtr3d ⊢ ( 𝜑 → ( 𝐷 −ℎ 𝐵 ) = 0ℎ )
33 hvsubeq0 ⊢ ( ( 𝐷 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐷 −ℎ 𝐵 ) = 0ℎ ↔ 𝐷 = 𝐵 ) )
34 18 14 33 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 −ℎ 𝐵 ) = 0ℎ ↔ 𝐷 = 𝐵 ) )
35 32 34 mpbid ⊢ ( 𝜑 → 𝐷 = 𝐵 )
36 35 eqcomd ⊢ ( 𝜑 → 𝐵 = 𝐷 )
37 31 36 jca ⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )