Metamath Proof Explorer

Theorem h1de2i

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 ${⊢}{A}\in ℋ$
h1de2.2 ${⊢}{B}\in ℋ$
Assertion h1de2i ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}$

Proof

Step Hyp Ref Expression
1 h1de2.1 ${⊢}{A}\in ℋ$
2 h1de2.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 his2sub ${⊢}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in ℋ\wedge \left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\in ℋ\wedge {A}\in ℋ\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}}{A}=\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{A}\right)$
8 4 6 1 7 mp3an ${⊢}\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}}{A}=\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{A}\right)$
9 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)$
10 3 1 1 9 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)$
11 1 1 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
12 3 11 mulcomi ${⊢}\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)$
13 10 12 eqtri ${⊢}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}=\left({A}{\cdot }_{\mathrm{ih}}{A}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right)$
14 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)$
15 5 2 1 14 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)$
16 13 15 oveq12i ${⊢}\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{A}\right)=\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)$
17 8 16 eqtr2i ${⊢}\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)=\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}}{A}$
18 his2sub ${⊢}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in ℋ\wedge \left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\in ℋ\wedge {B}\in ℋ\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}}{B}=\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}\right)$
19 4 6 2 18 mp3an ${⊢}\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}}{B}=\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}\right)$
20 3 5 mulcomi ${⊢}\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}}{B}\right)$
21 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)$
22 3 1 2 21 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)$
23 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)$
24 5 2 2 23 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)$
25 20 22 24 3eqtr4i ${⊢}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}=\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}$
26 4 2 hicli ${⊢}\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}\in ℂ$
27 6 2 hicli ${⊢}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}\in ℂ$
28 26 27 subeq0i ${⊢}\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}\right)=0↔\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}=\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}$
29 25 28 mpbir ${⊢}\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}\right)-\left(\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{B}\right)=0$
30 19 29 eqtri ${⊢}\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}}{B}=0$
31 2 h1dei ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\left({A}\in ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
32 1 31 mpbiran ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
33 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 ℋ$
34 oveq2 ${⊢}{x}=\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\to {B}{\cdot }_{\mathrm{ih}}{x}={B}{\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)$
35 34 eqeq1d ${⊢}{x}=\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\to \left({B}{\cdot }_{\mathrm{ih}}{x}=0↔{B}{\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\right)$
36 oveq2 ${⊢}{x}=\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\to {A}{\cdot }_{\mathrm{ih}}{x}={A}{\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)$
37 36 eqeq1d ${⊢}{x}=\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{x}=0↔{A}{\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\right)$
38 35 37 imbi12d ${⊢}{x}=\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\to \left(\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)↔\left({B}{\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\to {A}{\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\right)\right)$
39 38 rspcv ${⊢}\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(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\to \left({B}{\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\to {A}{\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\right)\right)$
40 33 39 ax-mp ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({B}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\to \left({B}{\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\to {A}{\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\right)$
41 32 40 sylbi ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \left({B}{\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\to {A}{\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\right)$
42 orthcom ${⊢}\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\in ℋ\wedge {B}\in ℋ\right)\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}}{B}=0↔{B}{\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\right)$
43 33 2 42 mp2an ${⊢}\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}}{B}=0↔{B}{\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$
44 orthcom ${⊢}\left(\left(\left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right){-}_{ℎ}\left(\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}\right)\in ℋ\wedge {A}\in ℋ\right)\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}}{A}=0↔{A}{\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\right)$
45 33 1 44 mp2an ${⊢}\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}}{A}=0↔{A}{\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$
46 41 43 45 3imtr4g ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\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}}{B}=0\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}}{A}=0\right)$
47 30 46 mpi ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\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}}{A}=0$
48 17 47 syl5eq ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\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)=0$
49 11 3 mulcli ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)\left({B}{\cdot }_{\mathrm{ih}}{B}\right)\in ℂ$
50 2 1 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
51 5 50 mulcli ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\in ℂ$
52 49 51 subeq0i ${⊢}\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)=0↔\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)$
53 48 52 sylib ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\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)$
54 53 eqcomd ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\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)$
55 1 2 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}$
56 54 55 sylib ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \left({B}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({A}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{B}$