axhvass-zf - Hilbert Space Explorer

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

Theorem axhvass-zf 28300

Description: Derive axiom ax-hvass 28318 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
axhil.1	⊢ 𝑈 = ⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩
axhil.2	⊢ 𝑈 ∈ CHil_OLD

**Assertion**
Ref	Expression
axhvass-zf	⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +_ℎ 𝐵) +_ℎ 𝐶) = (𝐴 +_ℎ (𝐵 +_ℎ 𝐶)))

**Proof of Theorem axhvass-zf**
Step	Hyp	Ref	Expression
1		axhil.2	. 2 ⊢ 𝑈 ∈ CHil_OLD
2		df-hba 28285	. . . 4 ⊢ ℋ = (BaseSet‘⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩)
3		axhil.1	. . . . 5 ⊢ 𝑈 = ⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩
4	3	fveq2i 6380	. . . 4 ⊢ (BaseSet‘𝑈) = (BaseSet‘⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩)
5	2, 4	eqtr4i 2790	. . 3 ⊢ ℋ = (BaseSet‘𝑈)
6	1	hlnvi 28207	. . . 4 ⊢ 𝑈 ∈ NrmCVec
7	3, 6	h2hva 28290	. . 3 ⊢ +_ℎ = ( +_𝑣 ‘𝑈)
8	5, 7	hlass 28216	. 2 ⊢ ((𝑈 ∈ CHil_OLD ∧ (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → ((𝐴 +_ℎ 𝐵) +_ℎ 𝐶) = (𝐴 +_ℎ (𝐵 +_ℎ 𝐶)))
9	1, 8	mpan 681	1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +_ℎ 𝐵) +_ℎ 𝐶) = (𝐴 +_ℎ (𝐵 +_ℎ 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ⟨cop 4342 ‘cfv 6070 (class class class)co 6844 BaseSetcba 27900 CHil_OLDchlo 28200 ℋchba 28235 +_ℎ cva 28236 ·_ℎ csm 28237 norm_ℎcno 28239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4932 ax-sep 4943 ax-nul 4951 ax-pow 5003 ax-pr 5064 ax-un 7149

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-ral 3060 df-rex 3061 df-reu 3062 df-rab 3064 df-v 3352 df-sbc 3599 df-csb 3694 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-nul 4082 df-if 4246 df-sn 4337 df-pr 4339 df-op 4343 df-uni 4597 df-iun 4680 df-br 4812 df-opab 4874 df-mpt 4891 df-id 5187 df-xp 5285 df-rel 5286 df-cnv 5287 df-co 5288 df-dm 5289 df-rn 5290 df-res 5291 df-ima 5292 df-iota 6033 df-fun 6072 df-fn 6073 df-f 6074 df-f1 6075 df-fo 6076 df-f1o 6077 df-fv 6078 df-ov 6847 df-oprab 6848 df-1st 7368 df-2nd 7369 df-grpo 27807 df-ablo 27859 df-vc 27873 df-nv 27906 df-va 27909 df-ba 27910 df-sm 27911 df-0v 27912 df-nmcv 27914 df-cbn 28178 df-hlo 28201 df-hba 28285

This theorem is referenced by: (None)

W3C validator