bcseqi

Description: Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL . (Contributed by NM, 16-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normlem7t.1	⊢ 𝐴 ∈ ℋ
	normlem7t.2	⊢ 𝐵 ∈ ℋ
Assertion	bcseqi	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) ↔ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		normlem7t.1	⊢ 𝐴 ∈ ℋ
2		normlem7t.2	⊢ 𝐵 ∈ ℋ
3	2 2	hicli	⊢ ( 𝐵 ·_ih 𝐵 ) ∈ ℂ
4	3 1	hvmulcli	⊢ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ
5	1 2	hicli	⊢ ( 𝐴 ·_ih 𝐵 ) ∈ ℂ
6	5 2	hvmulcli	⊢ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ
7	4 6 4 6	normlem9	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) − ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) )
8		oveq1	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) )
9	8	eqcomd	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) ) )
10		his5	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) ) )
11	3 4 1 10	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) )
12		hiidrcl	⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ·_ih 𝐵 ) ∈ ℝ )
13		cjre	⊢ ( ( 𝐵 ·_ih 𝐵 ) ∈ ℝ → ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) = ( 𝐵 ·_ih 𝐵 ) )
14	2 12 13	mp2b	⊢ ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) = ( 𝐵 ·_ih 𝐵 )
15		ax-his3	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) )
16	3 1 1 15	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) )
17	14 16	oveq12i	⊢ ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) )
18	1 1	hicli	⊢ ( 𝐴 ·_ih 𝐴 ) ∈ ℂ
19	3 18	mulcli	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) ∈ ℂ
20	3 19	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) ) = ( ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
21	18 3	mulcomi	⊢ ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) )
22	21	oveq1i	⊢ ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
23	20 22	eqtr4i	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) ) = ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) )
24	11 17 23	3eqtri	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) )
25		his5	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) ) )
26	5 4 2 25	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) )
27	2 1	his1i	⊢ ( 𝐵 ·_ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) )
28	27	eqcomi	⊢ ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) = ( 𝐵 ·_ih 𝐴 )
29		ax-his3	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) )
30	3 1 2 29	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) )
31	28 30	oveq12i	⊢ ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) ) = ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) )
32	2 1	hicli	⊢ ( 𝐵 ·_ih 𝐴 ) ∈ ℂ
33	3 5	mulcli	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) ∈ ℂ
34	32 33	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) ) = ( ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐴 ) )
35	3 5 32	mulassi	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
36	5 32	mulcli	⊢ ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ∈ ℂ
37	3 36	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
38	34 35 37	3eqtri	⊢ ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
39	26 31 38	3eqtri	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
40	9 24 39	3eqtr4g	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) )
41		ax-his3	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
42	5 2 1 41	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) )
43	14 42	oveq12i	⊢ ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
44		his5	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) ) )
45	3 6 1 44	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) )
46		his5	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ) )
47	5 6 2 46	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) )
48		ax-his3	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) )
49	5 2 2 48	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) )
50	28 49	oveq12i	⊢ ( ( ∗ ‘ ( 𝐴 ·_ih 𝐵 ) ) · ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ) = ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) )
51	5 3	mulcli	⊢ ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ
52	32 51	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐴 ) )
53	5 3 32	mul32i	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) )
54	36 3	mulcomi	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
55	52 53 54	3eqtri	⊢ ( ( 𝐵 ·_ih 𝐴 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
56	47 50 55	3eqtri	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( 𝐵 ·_ih 𝐵 ) · ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
57	43 45 56	3eqtr4ri	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) )
58	57	a1i	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) )
59	40 58	oveq12d	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) )
60	59	oveq1d	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) − ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) ) = ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) − ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) ) )
61	4 6	hicli	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℂ
62	6 4	hicli	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ∈ ℂ
63	61 62	addcli	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) ∈ ℂ
64	63	subidi	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) − ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) ) = 0
65	60 64	eqtrdi	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) − ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) + ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) ) ) = 0 )
66	7 65	syl5eq	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 )
67	4 6	hvsubcli	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ
68		his6	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ↔ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = 0_ℎ ) )
69	67 68	ax-mp	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ↔ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = 0_ℎ )
70	66 69	sylib	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = 0_ℎ )
71	4 6	hvsubeq0i	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = 0_ℎ ↔ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )
72	70 71	sylib	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) → ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )
73		oveq1	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) )
74	21 16	eqtr4i	⊢ ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 )
75	42	eqcomi	⊢ ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 )
76	73 74 75	3eqtr4g	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) → ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
77	76	eqcomd	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) → ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) )
78	72 77	impbii	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) ↔ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )

Metamath Proof Explorer

Theorem bcseqi

Proof