Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem bcseq 5073

Description: Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcs 5101.

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

**Assertion**
Ref	Expression
bcseq	⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) ↔ ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))

**Proof of Theorem bcseq**
Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . . . . . . 10 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((A ·_i B) · (B ·_i A)) · (B ·_i B)) = (((A ·_i A) · (B ·_i B)) · (B ·_i B)))
2	1	cleqcomd 1106	. . . . . . . . 9 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((A ·_i A) · (B ·_i B)) · (B ·_i B)) = (((A ·_i B) · (B ·_i A)) · (B ·_i B)))
3		normlem8.2	. . . . . . . . . . . 12 ⊢ B ∈ ℋ
4	3, 3	hicl 5044	. . . . . . . . . . 11 ⊢ (B ·_i B) ∈ ℂ
5		normlem8.1	. . . . . . . . . . . 12 ⊢ A ∈ ℋ
6	4, 5	hvmulcl 4990	. . . . . . . . . . 11 ⊢ ((B ·_i B) ·_s A) ∈ ℋ
7		his5 5050	. . . . . . . . . . 11 ⊢ (((B ·_i B) ∈ ℂ ∧ ((B ·_i B) ·_s A) ∈ ℋ ∧ A ∈ ℋ ) → (((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) = ((∗ ‘(B ·_i B)) · (((B ·_i B) ·_s A) ·_i A)))
8	4, 6, 5, 7	mp3an 642	. . . . . . . . . 10 ⊢ (((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) = ((∗ ‘(B ·_i B)) · (((B ·_i B) ·_s A) ·_i A))
9		hiidrclt 5053	. . . . . . . . . . . . 13 ⊢ (B ∈ ℋ → (B ·_i B) ∈ ℝ)
10	3, 9	ax-mp 6	. . . . . . . . . . . 12 ⊢ (B ·_i B) ∈ ℝ
11		cjret 4829	. . . . . . . . . . . 12 ⊢ ((B ·_i B) ∈ ℝ → (∗ ‘(B ·_i B)) = (B ·_i B))
12	10, 11	ax-mp 6	. . . . . . . . . . 11 ⊢ (∗ ‘(B ·_i B)) = (B ·_i B)
13		ax-his3 5047	. . . . . . . . . . . 12 ⊢ (((B ·_i B) ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ ) → (((B ·_i B) ·_s A) ·_i A) = ((B ·_i B) · (A ·_i A)))
14	4, 5, 5, 13	mp3an 642	. . . . . . . . . . 11 ⊢ (((B ·_i B) ·_s A) ·_i A) = ((B ·_i B) · (A ·_i A))
15	12, 14	opreq12i 3011	. . . . . . . . . 10 ⊢ ((∗ ‘(B ·_i B)) · (((B ·_i B) ·_s A) ·_i A)) = ((B ·_i B) · ((B ·_i B) · (A ·_i A)))
16	5, 5	hicl 5044	. . . . . . . . . . . . 13 ⊢ (A ·_i A) ∈ ℂ
17	4, 16	mulcl 4105	. . . . . . . . . . . 12 ⊢ ((B ·_i B) · (A ·_i A)) ∈ ℂ
18	4, 17	mulcom 4107	. . . . . . . . . . 11 ⊢ ((B ·_i B) · ((B ·_i B) · (A ·_i A))) = (((B ·_i B) · (A ·_i A)) · (B ·_i B))
19	16, 4	mulcom 4107	. . . . . . . . . . . 12 ⊢ ((A ·_i A) · (B ·_i B)) = ((B ·_i B) · (A ·_i A))
20	19	opreq1i 3009	. . . . . . . . . . 11 ⊢ (((A ·_i A) · (B ·_i B)) · (B ·_i B)) = (((B ·_i B) · (A ·_i A)) · (B ·_i B))
21	18, 20	eqtr4 1122	. . . . . . . . . 10 ⊢ ((B ·_i B) · ((B ·_i B) · (A ·_i A))) = (((A ·_i A) · (B ·_i B)) · (B ·_i B))
22	8, 15, 21	3eqtr 1123	. . . . . . . . 9 ⊢ (((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) = (((A ·_i A) · (B ·_i B)) · (B ·_i B))
23	5, 3	hicl 5044	. . . . . . . . . . 11 ⊢ (A ·_i B) ∈ ℂ
24		his5 5050	. . . . . . . . . . 11 ⊢ (((A ·_i B) ∈ ℂ ∧ ((B ·_i B) ·_s A) ∈ ℋ ∧ B ∈ ℋ ) → (((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) = ((∗ ‘(A ·_i B)) · (((B ·_i B) ·_s A) ·_i B)))
25	23, 6, 3, 24	mp3an 642	. . . . . . . . . 10 ⊢ (((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) = ((∗ ‘(A ·_i B)) · (((B ·_i B) ·_s A) ·_i B))
26		ax-his1 5045	. . . . . . . . . . . . 13 ⊢ ((B ∈ ℋ ∧ A ∈ ℋ ) → (B ·_i A) = (∗ ‘(A ·_i B)))
27	3, 5, 26	mp2an 520	. . . . . . . . . . . 12 ⊢ (B ·_i A) = (∗ ‘(A ·_i B))
28	27	cleqcomi 1105	. . . . . . . . . . 11 ⊢ (∗ ‘(A ·_i B)) = (B ·_i A)
29		ax-his3 5047	. . . . . . . . . . . 12 ⊢ (((B ·_i B) ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ ) → (((B ·_i B) ·_s A) ·_i B) = ((B ·_i B) · (A ·_i B)))
30	4, 5, 3, 29	mp3an 642	. . . . . . . . . . 11 ⊢ (((B ·_i B) ·_s A) ·_i B) = ((B ·_i B) · (A ·_i B))
31	28, 30	opreq12i 3011	. . . . . . . . . 10 ⊢ ((∗ ‘(A ·_i B)) · (((B ·_i B) ·_s A) ·_i B)) = ((B ·_i A) · ((B ·_i B) · (A ·_i B)))
32	3, 5	hicl 5044	. . . . . . . . . . . 12 ⊢ (B ·_i A) ∈ ℂ
33	4, 23	mulcl 4105	. . . . . . . . . . . 12 ⊢ ((B ·_i B) · (A ·_i B)) ∈ ℂ
34	32, 33	mulcom 4107	. . . . . . . . . . 11 ⊢ ((B ·_i A) · ((B ·_i B) · (A ·_i B))) = (((B ·_i B) · (A ·_i B)) · (B ·_i A))
35	4, 23, 32	mulass 4109	. . . . . . . . . . 11 ⊢ (((B ·_i B) · (A ·_i B)) · (B ·_i A)) = ((B ·_i B) · ((A ·_i B) · (B ·_i A)))
36	23, 32	mulcl 4105	. . . . . . . . . . . 12 ⊢ ((A ·_i B) · (B ·_i A)) ∈ ℂ
37	4, 36	mulcom 4107	. . . . . . . . . . 11 ⊢ ((B ·_i B) · ((A ·_i B) · (B ·_i A))) = (((A ·_i B) · (B ·_i A)) · (B ·_i B))
38	34, 35, 37	3eqtr 1123	. . . . . . . . . 10 ⊢ ((B ·_i A) · ((B ·_i B) · (A ·_i B))) = (((A ·_i B) · (B ·_i A)) · (B ·_i B))
39	25, 31, 38	3eqtr 1123	. . . . . . . . 9 ⊢ (((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) = (((A ·_i B) · (B ·_i A)) · (B ·_i B))
40	2, 22, 39	3eqtr4g 1147	. . . . . . . 8 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) = (((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)))
41		ax-his3 5047	. . . . . . . . . . . 12 ⊢ (((A ·_i B) ∈ ℂ ∧ B ∈ ℋ ∧ A ∈ ℋ ) → (((A ·_i B) ·_s B) ·_i A) = ((A ·_i B) · (B ·_i A)))
42	23, 3, 5, 41	mp3an 642	. . . . . . . . . . 11 ⊢ (((A ·_i B) ·_s B) ·_i A) = ((A ·_i B) · (B ·_i A))
43	12, 42	opreq12i 3011	. . . . . . . . . 10 ⊢ ((∗ ‘(B ·_i B)) · (((A ·_i B) ·_s B) ·_i A)) = ((B ·_i B) · ((A ·_i B) · (B ·_i A)))
44	23, 3	hvmulcl 4990	. . . . . . . . . . 11 ⊢ ((A ·_i B) ·_s B) ∈ ℋ
45		his5 5050	. . . . . . . . . . 11 ⊢ (((B ·_i B) ∈ ℂ ∧ ((A ·_i B) ·_s B) ∈ ℋ ∧ A ∈ ℋ ) → (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)) = ((∗ ‘(B ·_i B)) · (((A ·_i B) ·_s B) ·_i A)))
46	4, 44, 5, 45	mp3an 642	. . . . . . . . . 10 ⊢ (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)) = ((∗ ‘(B ·_i B)) · (((A ·_i B) ·_s B) ·_i A))
47		his5 5050	. . . . . . . . . . . 12 ⊢ (((A ·_i B) ∈ ℂ ∧ ((A ·_i B) ·_s B) ∈ ℋ ∧ B ∈ ℋ ) → (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B)) = ((∗ ‘(A ·_i B)) · (((A ·_i B) ·_s B) ·_i B)))
48	23, 44, 3, 47	mp3an 642	. . . . . . . . . . 11 ⊢ (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B)) = ((∗ ‘(A ·_i B)) · (((A ·_i B) ·_s B) ·_i B))
49		ax-his3 5047	. . . . . . . . . . . . 13 ⊢ (((A ·_i B) ∈ ℂ ∧ B ∈ ℋ ∧ B ∈ ℋ ) → (((A ·_i B) ·_s B) ·_i B) = ((A ·_i B) · (B ·_i B)))
50	23, 3, 3, 49	mp3an 642	. . . . . . . . . . . 12 ⊢ (((A ·_i B) ·_s B) ·_i B) = ((A ·_i B) · (B ·_i B))
51	28, 50	opreq12i 3011	. . . . . . . . . . 11 ⊢ ((∗ ‘(A ·_i B)) · (((A ·_i B) ·_s B) ·_i B)) = ((B ·_i A) · ((A ·_i B) · (B ·_i B)))
52	23, 4	mulcl 4105	. . . . . . . . . . . . 13 ⊢ ((A ·_i B) · (B ·_i B)) ∈ ℂ
53	32, 52	mulcom 4107	. . . . . . . . . . . 12 ⊢ ((B ·_i A) · ((A ·_i B) · (B ·_i B))) = (((A ·_i B) · (B ·_i B)) · (B ·_i A))
54	23, 4, 32	mul23 4179	. . . . . . . . . . . 12 ⊢ (((A ·_i B) · (B ·_i B)) · (B ·_i A)) = (((A ·_i B) · (B ·_i A)) · (B ·_i B))
55	36, 4	mulcom 4107	. . . . . . . . . . . 12 ⊢ (((A ·_i B) · (B ·_i A)) · (B ·_i B)) = ((B ·_i B) · ((A ·_i B) · (B ·_i A)))
56	53, 54, 55	3eqtr 1123	. . . . . . . . . . 11 ⊢ ((B ·_i A) · ((A ·_i B) · (B ·_i B))) = ((B ·_i B) · ((A ·_i B) · (B ·_i A)))
57	48, 51, 56	3eqtr 1123	. . . . . . . . . 10 ⊢ (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B)) = ((B ·_i B) · ((A ·_i B) · (B ·_i A)))
58	43, 46, 57	3eqtr4r 1127	. . . . . . . . 9 ⊢ (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B)) = (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))
59	58	a1i 7	. . . . . . . 8 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B)) = (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)))
60	40, 59	opreq12d 3014	. . . . . . 7 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → ((((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) + (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B))) = ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))))
61	60	opreq1d 3012	. . . . . 6 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) + (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B))) − ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)))) = (((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))) − ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)))))
62	6, 44	hicl 5044	. . . . . . . 8 ⊢ (((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) ∈ ℂ
63	44, 6	hicl 5044	. . . . . . . 8 ⊢ (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)) ∈ ℂ
64	62, 63	addcl 4104	. . . . . . 7 ⊢ ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))) ∈ ℂ
65	64	subid 4155	. . . . . 6 ⊢ (((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))) − ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)))) = 0
66	61, 65	syl6eq 1140	. . . . 5 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) + (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B))) − ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A)))) = 0)
67	6, 44	normlem8 5071	. . . . 5 ⊢ ((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ·_i (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B))) = (((((B ·_i B) ·_s A) ·_i ((B ·_i B) ·_s A)) + (((A ·_i B) ·_s B) ·_i ((A ·_i B) ·_s B))) − ((((B ·_i B) ·_s A) ·_i ((A ·_i B) ·_s B)) + (((A ·_i B) ·_s B) ·_i ((B ·_i B) ·_s A))))
68	66, 67	syl5eq 1136	. . . 4 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → ((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ·_i (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B))) = 0)
69	6, 44	hvsubcl 5002	. . . . 5 ⊢ (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ∈ ℋ
70		his6 5057	. . . . 5 ⊢ ((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ∈ ℋ → (((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ·_i (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B))) = 0 ↔ (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) = 0_v))
71	69, 70	ax-mp 6	. . . 4 ⊢ (((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) ·_i (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B))) = 0 ↔ (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) = 0_v)
72	68, 71	sylib 173	. . 3 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → (((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) = 0_v)
73	6, 44	hvsubeq0 5035	. . 3 ⊢ ((((B ·_i B) ·_s A) −_v ((A ·_i B) ·_s B)) = 0_v ↔ ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))
74	72, 73	sylib 173	. 2 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) → ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))
75		opreq1 3006	. . . 4 ⊢ (((B ·_i B) ·_s A) = ((A ·_i B) ·_s B) → (((B ·_i B) ·_s A) ·_i A) = (((A ·_i B) ·_s B) ·_i A))
76	19, 14	eqtr4 1122	. . . 4 ⊢ ((A ·_i A) · (B ·_i B)) = (((B ·_i B) ·_s A) ·_i A)
77	42	cleqcomi 1105	. . . 4 ⊢ ((A ·_i B) · (B ·_i A)) = (((A ·_i B) ·_s B) ·_i A)
78	75, 76, 77	3eqtr4g 1147	. . 3 ⊢ (((B ·_i B) ·_s A) = ((A ·_i B) ·_s B) → ((A ·_i A) · (B ·_i B)) = ((A ·_i B) · (B ·_i A)))
79	78	cleqcomd 1106	. 2 ⊢ (((B ·_i B) ·_s A) = ((A ·_i B) ·_s B) → ((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)))
80	74, 79	impbi 139	1 ⊢ (((A ·_i B) · (B ·_i A)) = ((A ·_i A) · (B ·_i B)) ↔ ((B ·_i B) ·_s A) = ((A ·_i B) ·_s B))

Colors of variables: wff set class

Syntax hints: ↔ wb 127 = wceq 1091 ∈ wcel 1092 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 + caddc 4031 · cmulc 4032 − cmin 4089 ∗ccj 4788 ℋ chil 4958 ·_s csm 4960 0_vc0v 4961 −_v cmv 4962 ·_i csp 4963

This theorem is referenced by: h1de2 5458

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-hvaddcl 4984 ax-hvcom 4985 ax-hvass 4986 ax-hvzercl 4987 ax-hvaddid 4988 ax-hvmulcl 4989 ax-hvmulid 4991 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-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-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 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-re 4790 df-im 4791 df-cj 4792 df-hvsub 4996

metamath.org