Theorem pjhthmo 28747

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.)

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem pjhthmo

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		an4 646	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) ↔ ((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))))
2		reeanv 3292	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) ↔ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)))
3		simpll1 1226	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐴 ∈ Sℋ )
4		simpll2 1228	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐵 ∈ Sℋ )
5		simpll3 1230	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝐴 ∩ 𝐵) = 0ℋ)
6		simplrl 767	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑥 ∈ 𝐴)
7		simprll 769	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑦 ∈ 𝐵)
8		simplrr 768	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑧 ∈ 𝐴)
9		simprlr 770	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑤 ∈ 𝐵)
10		simprrl 771	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐶 = (𝑥 +ℎ 𝑦))
11		simprrr 772	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝐶 = (𝑧 +ℎ 𝑤))
12	10, 11	eqtr3d 2815	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤))
13	3, 4, 5, 6, 7, 8, 9, 12	shuni 28745	. . . . . . . . 9 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))
14	13	simpld 490	. . . . . . . 8 ⊢ ((((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)))) → 𝑥 = 𝑧)
15	14	exp32 413	. . . . . . 7 ⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧)))
16	15	rexlimdvv 3219	. . . . . 6 ⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (∃𝑦 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (𝐶 = (𝑥 +ℎ 𝑦) ∧ 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))
17	2, 16	syl5bir 235	. . . . 5 ⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)) → 𝑥 = 𝑧))
18	17	expimpd 447	. . . 4 ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧))
19	1, 18	syl5bir 235	. . 3 ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧))
20	19	alrimivv 1971	. 2 ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧))
21		eleq1w 2841	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
22		oveq1 6929	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑦))
23	22	eqeq2d 2787	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝐶 = (𝑥 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑦)))
24	23	rexbidv 3236	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑦)))
25		oveq2 6930	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (𝑧 +ℎ 𝑦) = (𝑧 +ℎ 𝑤))
26	25	eqeq2d 2787	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝐶 = (𝑧 +ℎ 𝑦) ↔ 𝐶 = (𝑧 +ℎ 𝑤)))
27	26	cbvrexv 3367	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))
28	24, 27	syl6bb 279	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦) ↔ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤)))
29	21, 28	anbi12d 624	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))))
30	29	mo4 2584	. 2 ⊢ (∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐴 ∧ ∃𝑤 ∈ 𝐵 𝐶 = (𝑧 +ℎ 𝑤))) → 𝑥 = 𝑧))
31	20, 30	sylibr 226	1 ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)))

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071  ∀wal 1599   = wceq 1601   ∈ wcel 2106  ∃*wmo 2548  ∃wrex 3090   ∩ cin 3790  (class class class)co 6922   +_ℎ cva 28363   S_ℋ csh 28371  0_ℋc0h 28378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-hilex 28442  ax-hfvadd 28443  ax-hvcom 28444  ax-hvass 28445  ax-hv0cl 28446  ax-hvaddid 28447  ax-hfvmul 28448  ax-hvmulid 28449  ax-hvmulass 28450  ax-hvdistr1 28451  ax-hvdistr2 28452  ax-hvmul0 28453

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-hvsub 28414  df-sh 28650  df-ch0 28696

This theorem is referenced by:  pjhtheu  28839  pjpreeq  28843