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 ⊢ φ → H ∈ S ℋ
shuni.2 ⊢ φ → K ∈ S ℋ
shuni.3 ⊢ φ → H ∩ K = 0 ℋ
shuni.4 ⊢ φ → A ∈ H
shuni.5 ⊢ φ → B ∈ K
shuni.6 ⊢ φ → C ∈ H
shuni.7 ⊢ φ → D ∈ K
shuni.8 ⊢ φ → A + ℎ B = C + ℎ D
Assertion shuni ⊢ φ → A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 shuni.1 ⊢ φ → H ∈ S ℋ
2 shuni.2 ⊢ φ → K ∈ S ℋ
3 shuni.3 ⊢ φ → H ∩ K = 0 ℋ
4 shuni.4 ⊢ φ → A ∈ H
5 shuni.5 ⊢ φ → B ∈ K
6 shuni.6 ⊢ φ → C ∈ H
7 shuni.7 ⊢ φ → D ∈ K
8 shuni.8 ⊢ φ → A + ℎ B = C + ℎ D
9 shsubcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ C ∈ H → A - ℎ C ∈ H
10 1 4 6 9 syl3anc ⊢ φ → A - ℎ C ∈ H
11 shel ⊢ H ∈ S ℋ ∧ A ∈ H → A ∈ ℋ
12 1 4 11 syl2anc ⊢ φ → A ∈ ℋ
13 shel ⊢ K ∈ S ℋ ∧ B ∈ K → B ∈ ℋ
14 2 5 13 syl2anc ⊢ φ → B ∈ ℋ
15 shel ⊢ H ∈ S ℋ ∧ C ∈ H → C ∈ ℋ
16 1 6 15 syl2anc ⊢ φ → C ∈ ℋ
17 shel ⊢ K ∈ S ℋ ∧ D ∈ K → D ∈ ℋ
18 2 7 17 syl2anc ⊢ φ → D ∈ ℋ
19 hvaddsub4 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B = C + ℎ D ↔ A - ℎ C = D - ℎ B
20 12 14 16 18 19 syl22anc ⊢ φ → A + ℎ B = C + ℎ D ↔ A - ℎ C = D - ℎ B
21 8 20 mpbid ⊢ φ → A - ℎ C = D - ℎ B
22 shsubcl ⊢ K ∈ S ℋ ∧ D ∈ K ∧ B ∈ K → D - ℎ B ∈ K
23 2 7 5 22 syl3anc ⊢ φ → D - ℎ B ∈ K
24 21 23 eqeltrd ⊢ φ → A - ℎ C ∈ K
25 10 24 elind ⊢ φ → A - ℎ C ∈ H ∩ K
26 25 3 eleqtrd ⊢ φ → A - ℎ C ∈ 0 ℋ
27 elch0 ⊢ A - ℎ C ∈ 0 ℋ ↔ A - ℎ C = 0 ℎ
28 26 27 sylib ⊢ φ → A - ℎ C = 0 ℎ
29 hvsubeq0 ⊢ A ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = 0 ℎ ↔ A = C
30 12 16 29 syl2anc ⊢ φ → A - ℎ C = 0 ℎ ↔ A = C
31 28 30 mpbid ⊢ φ → A = C
32 21 28 eqtr3d ⊢ φ → D - ℎ B = 0 ℎ
33 hvsubeq0 ⊢ D ∈ ℋ ∧ B ∈ ℋ → D - ℎ B = 0 ℎ ↔ D = B
34 18 14 33 syl2anc ⊢ φ → D - ℎ B = 0 ℎ ↔ D = B
35 32 34 mpbid ⊢ φ → D = B
36 35 eqcomd ⊢ φ → B = D
37 31 36 jca ⊢ φ → A = C ∧ B = D