chocunii - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > chocunii		Structured version Visualization version GIF version

Theorem chocunii 31388

Description: Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of [Beran] p. 102 (uniqueness part). (Contributed by NM, 23-Oct-1999.) (Proof shortened by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
chocuni.1	⊢ 𝐻 ∈ C_ℋ

**Assertion**
Ref	Expression
chocunii	⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) → ((𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))

**Proof of Theorem chocunii**
Step	Hyp	Ref	Expression
1		chocuni.1	. . . . 5 ⊢ 𝐻 ∈ C_ℋ
2	1	chshii 31314	. . . 4 ⊢ 𝐻 ∈ S_ℋ
3	2	a1i 11	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → 𝐻 ∈ S_ℋ )
4		shocsh 31371	. . . 4 ⊢ (𝐻 ∈ S_ℋ → (⊥‘𝐻) ∈ S_ℋ )
5	2, 4	mp1i 13	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → (⊥‘𝐻) ∈ S_ℋ )
6		ocin 31383	. . . 4 ⊢ (𝐻 ∈ S_ℋ → (𝐻 ∩ (⊥‘𝐻)) = 0_ℋ)
7	2, 6	mp1i 13	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → (𝐻 ∩ (⊥‘𝐻)) = 0_ℋ)
8		simplll 775	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → 𝐴 ∈ 𝐻)
9		simpllr 776	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → 𝐵 ∈ (⊥‘𝐻))
10		simplrl 777	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → 𝐶 ∈ 𝐻)
11		simplrr 778	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → 𝐷 ∈ (⊥‘𝐻))
12		eqtr2 2758	. . . 4 ⊢ ((𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷)) → (𝐴 +_ℎ 𝐵) = (𝐶 +_ℎ 𝐷))
13	12	adantl 481	. . 3 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → (𝐴 +_ℎ 𝐵) = (𝐶 +_ℎ 𝐷))
14	3, 5, 7, 8, 9, 10, 11, 13	shuni 31387	. 2 ⊢ ((((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) ∧ (𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷))) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
15	14	ex 412	1 ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) → ((𝑅 = (𝐴 +_ℎ 𝐵) ∧ 𝑅 = (𝐶 +_ℎ 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∩ cin 3902 ‘cfv 6500 (class class class)co 7368 +_ℎ cva 31007 S_ℋ csh 31015 C_ℋ cch 31016 ⊥cort 31017 0_ℋc0h 31022

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-hilex 31086 ax-hfvadd 31087 ax-hvcom 31088 ax-hvass 31089 ax-hv0cl 31090 ax-hvaddid 31091 ax-hfvmul 31092 ax-hvmulid 31093 ax-hvmulass 31094 ax-hvdistr1 31095 ax-hvdistr2 31096 ax-hvmul0 31097 ax-hfi 31166 ax-his2 31170 ax-his3 31171 ax-his4 31172

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-po 5540 df-so 5541 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-hvsub 31058 df-sh 31294 df-ch 31308 df-oc 31339 df-ch0 31340

This theorem is referenced by: pjcompi 31759

W3C validator