Metamath Proof Explorer

Theorem pjhthmo

Description: Projection Theorem, uniqueness part. Any two disjoint subspaces yield a unique decomposition of vectors into each subspace. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhthmo ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) )
2 reeanv ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
3 simpll1 ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝐴 ∈ Sℋ )
4 simpll2 ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝐵 ∈ Sℋ )
5 simpll3 ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )
6 simplrl ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝑥 ∈ 𝐴 )
7 simprll ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝑦 ∈ 𝐵 )
8 simplrr ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝑧 ∈ 𝐴 )
9 simprlr ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝑤 ∈ 𝐵 )
10 simprrl ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝐶 = ( 𝑥 +ℎ 𝑦 ) )
11 simprrr ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝐶 = ( 𝑧 +ℎ 𝑤 ) )
12 10 11 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
13 3 4 5 6 7 8 9 12 shuni ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
14 13 simpld ⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) ) → 𝑥 = 𝑧 )
15 14 exp32 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) ) )
16 15 rexlimdvv ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
17 2 16 syl5bir ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 = 𝑧 ) )
18 17 expimpd ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
19 1 18 syl5bir ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
20 19 alrimivv ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∀ 𝑥 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
21 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
22 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑦 ) )
23 22 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ 𝐶 = ( 𝑧 +ℎ 𝑦 ) ) )
24 23 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑦 ) ) )
25 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
26 25 eqeq2d ⊢ ( 𝑦 = 𝑤 → ( 𝐶 = ( 𝑧 +ℎ 𝑦 ) ↔ 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
27 26 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) )
28 24 27 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) )
29 21 28 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) )
30 29 mo4 ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 𝐶 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
31 20 30 sylibr ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )