Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem h1de2b 5459

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector.

**Hypotheses**
Ref	Expression
h1de2.1	⊢ A ∈ ℋ
h1de2.2	⊢ B ∈ ℋ

**Assertion**
Ref	Expression
h1de2b	⊢ (¬ B = 0_v → (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ A = (((A ·_i B) / (B ·_i B)) ·_s B)))

**Proof of Theorem h1de2b**
Step	Hyp	Ref	Expression
1		df-ne 1192	. . 3 ⊢ ((B ·_i B) ≠ 0 ↔ ¬ (B ·_i B) = 0)
2		h1de2.2	. . . . 5 ⊢ B ∈ ℋ
3		his6 5057	. . . . 5 ⊢ (B ∈ ℋ → ((B ·_i B) = 0 ↔ B = 0_v))
4	2, 3	ax-mp 6	. . . 4 ⊢ ((B ·_i B) = 0 ↔ B = 0_v)
5	4	negbii 162	. . 3 ⊢ (¬ (B ·_i B) = 0 ↔ ¬ B = 0_v)
6	1, 5	bitr 151	. 2 ⊢ ((B ·_i B) ≠ 0 ↔ ¬ B = 0_v)
7		h1de2.1	. . . . . . . 8 ⊢ A ∈ ℋ
8	7, 2	h1de2 5458	. . . . . . 7 ⊢ (A ∈ (⊥ ‘(⊥ ‘{B})) → ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))
9	8	adantl 305	. . . . . 6 ⊢ (((B ·_i B) ≠ 0 ∧ A ∈ (⊥ ‘(⊥ ‘{B}))) → ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))
10	9	opreq2d 3013	. . . . 5 ⊢ (((B ·_i B) ≠ 0 ∧ A ∈ (⊥ ‘(⊥ ‘{B}))) → ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)) = ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)))
11		1cn 4101	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
12	2, 2	hicl 5044	. . . . . . . . . 10 ⊢ (B ·_i B) ∈ ℂ
13	11, 12	divclz 4222	. . . . . . . . 9 ⊢ ((B ·_i B) ≠ 0 → (1 / (B ·_i B)) ∈ ℂ)
14		ax-hvmulass 4992	. . . . . . . . . . 11 ⊢ (((1 / (B ·_i B)) ∈ ℂ ∧ (B ·_i B) ∈ ℂ ∧ A ∈ ℋ ) → (((1 / (B ·_i B)) · (B ·_i B)) ·_s A) = ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)))
15	12, 14	mp3an2 640	. . . . . . . . . 10 ⊢ (((1 / (B ·_i B)) ∈ ℂ ∧ A ∈ ℋ ) → (((1 / (B ·_i B)) · (B ·_i B)) ·_s A) = ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)))
16	7, 15	mpan2 519	. . . . . . . . 9 ⊢ ((1 / (B ·_i B)) ∈ ℂ → (((1 / (B ·_i B)) · (B ·_i B)) ·_s A) = ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)))
17	13, 16	syl 12	. . . . . . . 8 ⊢ ((B ·_i B) ≠ 0 → (((1 / (B ·_i B)) · (B ·_i B)) ·_s A) = ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)))
18	12, 11	divcan1z 4226	. . . . . . . . 9 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) · (B ·_i B)) = 1)
19	18	opreq1d 3012	. . . . . . . 8 ⊢ ((B ·_i B) ≠ 0 → (((1 / (B ·_i B)) · (B ·_i B)) ·_s A) = (1 ·_s A))
20	17, 19	eqtr3d 1130	. . . . . . 7 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)) = (1 ·_s A))
21		ax-hvmulid 4991	. . . . . . . 8 ⊢ (A ∈ ℋ → (1 ·_s A) = A)
22	7, 21	ax-mp 6	. . . . . . 7 ⊢ (1 ·_s A) = A
23	20, 22	syl6eq 1140	. . . . . 6 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)) = A)
24	23	adantr 306	. . . . 5 ⊢ (((B ·_i B) ≠ 0 ∧ A ∈ (⊥ ‘(⊥ ‘{B}))) → ((1 / (B ·_i B)) ·_s ((B ·_i B) ·_s A)) = A)
25	7, 2	hicl 5044	. . . . . . . . . 10 ⊢ (A ·_i B) ∈ ℂ
26		ax-hvmulass 4992	. . . . . . . . . 10 ⊢ (((1 / (B ·_i B)) ∈ ℂ ∧ (A ·_i B) ∈ ℂ ∧ B ∈ ℋ ) → (((1 / (B ·_i B)) · (A ·_i B)) ·_s B) = ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)))
27	25, 26	mp3an2 640	. . . . . . . . 9 ⊢ (((1 / (B ·_i B)) ∈ ℂ ∧ B ∈ ℋ ) → (((1 / (B ·_i B)) · (A ·_i B)) ·_s B) = ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)))
28	2, 27	mpan2 519	. . . . . . . 8 ⊢ ((1 / (B ·_i B)) ∈ ℂ → (((1 / (B ·_i B)) · (A ·_i B)) ·_s B) = ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)))
29	13, 28	syl 12	. . . . . . 7 ⊢ ((B ·_i B) ≠ 0 → (((1 / (B ·_i B)) · (A ·_i B)) ·_s B) = ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)))
30		axmulcom 4071	. . . . . . . . . . 11 ⊢ (((1 / (B ·_i B)) ∈ ℂ ∧ (A ·_i B) ∈ ℂ) → ((1 / (B ·_i B)) · (A ·_i B)) = ((A ·_i B) · (1 / (B ·_i B))))
31	25, 30	mpan2 519	. . . . . . . . . 10 ⊢ ((1 / (B ·_i B)) ∈ ℂ → ((1 / (B ·_i B)) · (A ·_i B)) = ((A ·_i B) · (1 / (B ·_i B))))
32	13, 31	syl 12	. . . . . . . . 9 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) · (A ·_i B)) = ((A ·_i B) · (1 / (B ·_i B))))
33	25, 12	divrecz 4237	. . . . . . . . 9 ⊢ ((B ·_i B) ≠ 0 → ((A ·_i B) / (B ·_i B)) = ((A ·_i B) · (1 / (B ·_i B))))
34	32, 33	eqtr4d 1131	. . . . . . . 8 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) · (A ·_i B)) = ((A ·_i B) / (B ·_i B)))
35	34	opreq1d 3012	. . . . . . 7 ⊢ ((B ·_i B) ≠ 0 → (((1 / (B ·_i B)) · (A ·_i B)) ·_s B) = (((A ·_i B) / (B ·_i B)) ·_s B))
36	29, 35	eqtr3d 1130	. . . . . 6 ⊢ ((B ·_i B) ≠ 0 → ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)) = (((A ·_i B) / (B ·_i B)) ·_s B))
37	36	adantr 306	. . . . 5 ⊢ (((B ·_i B) ≠ 0 ∧ A ∈ (⊥ ‘(⊥ ‘{B}))) → ((1 / (B ·_i B)) ·_s ((A ·_i B) ·_s B)) = (((A ·_i B) / (B ·_i B)) ·_s B))
38	10, 24, 37	3eqtr3d 1133	. . . 4 ⊢ (((B ·_i B) ≠ 0 ∧ A ∈ (⊥ ‘(⊥ ‘{B}))) → A = (((A ·_i B) / (B ·_i B)) ·_s B))
39	38	exp 291	. . 3 ⊢ ((B ·_i B) ≠ 0 → (A ∈ (⊥ ‘(⊥ ‘{B})) → A = (((A ·_i B) / (B ·_i B)) ·_s B)))
40		eleq1 1149	. . . . 5 ⊢ (A = (((A ·_i B) / (B ·_i B)) ·_s B) → (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ (((A ·_i B) / (B ·_i B)) ·_s B) ∈ (⊥ ‘(⊥ ‘{B}))))
41	25, 12	divclz 4222	. . . . . 6 ⊢ ((B ·_i B) ≠ 0 → ((A ·_i B) / (B ·_i B)) ∈ ℂ)
42		h1did 5456	. . . . . . . 8 ⊢ (B ∈ ℋ → B ∈ (⊥ ‘(⊥ ‘{B})))
43	2, 42	ax-mp 6	. . . . . . 7 ⊢ B ∈ (⊥ ‘(⊥ ‘{B}))
44		snssi 1851	. . . . . . . . . . . 12 ⊢ (B ∈ ℋ → {B} ⊆ ℋ )
45	2, 44	ax-mp 6	. . . . . . . . . . 11 ⊢ {B} ⊆ ℋ
46	45	occl 5188	. . . . . . . . . 10 ⊢ (⊥ ‘{B}) ∈ C_ℋ
47	46	chocl 5192	. . . . . . . . 9 ⊢ (⊥ ‘(⊥ ‘{B})) ∈ C_ℋ
48	47	chshi 5132	. . . . . . . 8 ⊢ (⊥ ‘(⊥ ‘{B})) ∈ S_ℋ
49		shmulclt 5124	. . . . . . . 8 ⊢ ((⊥ ‘(⊥ ‘{B})) ∈ S_ℋ → ((((A ·_i B) / (B ·_i B)) ∈ ℂ ∧ B ∈ (⊥ ‘(⊥ ‘{B}))) → (((A ·_i B) / (B ·_i B)) ·_s B) ∈ (⊥ ‘(⊥ ‘{B}))))
50	48, 49	ax-mp 6	. . . . . . 7 ⊢ ((((A ·_i B) / (B ·_i B)) ∈ ℂ ∧ B ∈ (⊥ ‘(⊥ ‘{B}))) → (((A ·_i B) / (B ·_i B)) ·_s B) ∈ (⊥ ‘(⊥ ‘{B})))
51	43, 50	mpan2 519	. . . . . 6 ⊢ (((A ·_i B) / (B ·_i B)) ∈ ℂ → (((A ·_i B) / (B ·_i B)) ·_s B) ∈ (⊥ ‘(⊥ ‘{B})))
52	41, 51	syl 12	. . . . 5 ⊢ ((B ·_i B) ≠ 0 → (((A ·_i B) / (B ·_i B)) ·_s B) ∈ (⊥ ‘(⊥ ‘{B})))
53	40, 52	syl5bir 184	. . . 4 ⊢ (A = (((A ·_i B) / (B ·_i B)) ·_s B) → ((B ·_i B) ≠ 0 → A ∈ (⊥ ‘(⊥ ‘{B}))))
54	53	com12 13	. . 3 ⊢ ((B ·_i B) ≠ 0 → (A = (((A ·_i B) / (B ·_i B)) ·_s B) → A ∈ (⊥ ‘(⊥ ‘{B}))))
55	39, 54	impbid 397	. 2 ⊢ ((B ·_i B) ≠ 0 → (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ A = (((A ·_i B) / (B ·_i B)) ·_s B)))
56	6, 55	sylbir 176	1 ⊢ (¬ B = 0_v → (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ A = (((A ·_i B) / (B ·_i B)) ·_s B)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 = wceq 1091 ∈ wcel 1092 ≠ wne 1190 ⊆ wss 1487 {csn 1808 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 0cc0 4028 1c1 4029 · cmulc 4032 / cdiv 4091 ℋ chil 4958 ·_s csm 4960 0_vc0v 4961 ·_i csp 4963 S_ℋ csh 4967 ⊥cort 4969

This theorem is referenced by: h1de2ctlem 5460 elspansn2t 5472

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-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-hilex 4983 ax-hvaddcl 4984 ax-hvcom 4985 ax-hvass 4986 ax-hvzercl 4987 ax-hvaddid 4988 ax-hvmulcl 4989 ax-hvmulid 4991 ax-hvmulass 4992 ax-hvdistr2 4994 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-abs 4793 df-clim 4876 df-hvsub 4996 df-hnorm 5074 df-hlim 5107 df-sh 5114 df-ch 5127 df-oc 5156

metamath.org