Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sh2 5126

Description: Subspace

of a Hilbert space.

**Assertion**
Ref	Expression
sh2	$/\$ $/\$

Distinct variable group(s):

**Proof of Theorem sh2**
Step	Hyp	Ref	Expression
1		anass 336	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2	1	baib 506	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
3		sh 5116	. 2 $/\$ $/\$ $/\$
4	2, 3	syl5bb 410	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 2

wb 127 $/\$ wa 196

wcel 1092

wral 1201

wss 1487 (class class class)co 3001

cc 4026

chil 4958

cva 4959

csm 4960

c0v 4961

csh 4967

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-hilex 4983

This theorem depends on definitions: df-bi 128 df-an 198 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-v 1349 df-in 1491 df-ss 1492 df-sh 5114