# Metamath Proof Explorer

## Theorem 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 ${⊢}{A}\in ℋ$
normlem7t.2 ${⊢}{B}\in ℋ$
Assertion bcseqi ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)=\left({A}{\cdot }_{\mathrm{ih}}{A}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right)↔\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}$

### Proof

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