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 ) → ∃* 𝑥 ( 𝑥𝐴 ∧ ∃ 𝑦𝐵 𝐶 = ( 𝑥 + 𝑦 ) ) )