# Metamath Proof Explorer

## Theorem h1de2ctlem

Description: Lemma for h1de2ci . (Contributed by NM, 19-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 ${⊢}{A}\in ℋ$
h1de2.2 ${⊢}{B}\in ℋ$
Assertion h1de2ctlem ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$

### Proof

Step Hyp Ref Expression
1 h1de2.1 ${⊢}{A}\in ℋ$
2 h1de2.2 ${⊢}{B}\in ℋ$
3 sneq ${⊢}{B}={0}_{ℎ}\to \left\{{B}\right\}=\left\{{0}_{ℎ}\right\}$
4 3 fveq2d ${⊢}{B}={0}_{ℎ}\to \perp \left(\left\{{B}\right\}\right)=\perp \left(\left\{{0}_{ℎ}\right\}\right)$
5 4 fveq2d ${⊢}{B}={0}_{ℎ}\to \perp \left(\perp \left(\left\{{B}\right\}\right)\right)=\perp \left(\perp \left(\left\{{0}_{ℎ}\right\}\right)\right)$
6 5 eleq2d ${⊢}{B}={0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{A}\in \perp \left(\perp \left(\left\{{0}_{ℎ}\right\}\right)\right)\right)$
7 1 elexi ${⊢}{A}\in \mathrm{V}$
8 7 elsn ${⊢}{A}\in \left\{{0}_{ℎ}\right\}↔{A}={0}_{ℎ}$
9 hsn0elch ${⊢}\left\{{0}_{ℎ}\right\}\in {\mathbf{C}}_{ℋ}$
10 9 ococi ${⊢}\perp \left(\perp \left(\left\{{0}_{ℎ}\right\}\right)\right)=\left\{{0}_{ℎ}\right\}$
11 10 eleq2i ${⊢}{A}\in \perp \left(\perp \left(\left\{{0}_{ℎ}\right\}\right)\right)↔{A}\in \left\{{0}_{ℎ}\right\}$
12 ax-hvmul0 ${⊢}{B}\in ℋ\to 0{\cdot }_{ℎ}{B}={0}_{ℎ}$
13 2 12 ax-mp ${⊢}0{\cdot }_{ℎ}{B}={0}_{ℎ}$
14 13 eqeq2i ${⊢}{A}=0{\cdot }_{ℎ}{B}↔{A}={0}_{ℎ}$
15 8 11 14 3bitr4ri ${⊢}{A}=0{\cdot }_{ℎ}{B}↔{A}\in \perp \left(\perp \left(\left\{{0}_{ℎ}\right\}\right)\right)$
16 6 15 syl6rbbr ${⊢}{B}={0}_{ℎ}\to \left({A}=0{\cdot }_{ℎ}{B}↔{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
17 0cn ${⊢}0\in ℂ$
18 oveq1 ${⊢}{x}=0\to {x}{\cdot }_{ℎ}{B}=0{\cdot }_{ℎ}{B}$
19 18 rspceeqv ${⊢}\left(0\in ℂ\wedge {A}=0{\cdot }_{ℎ}{B}\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$
20 17 19 mpan ${⊢}{A}=0{\cdot }_{ℎ}{B}\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$
21 16 20 syl6bir ${⊢}{B}={0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\right)$
22 1 2 h1de2bi ${⊢}{B}\ne {0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)$
23 his6 ${⊢}{B}\in ℋ\to \left({B}{\cdot }_{\mathrm{ih}}{B}=0↔{B}={0}_{ℎ}\right)$
24 2 23 ax-mp ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}=0↔{B}={0}_{ℎ}$
25 24 necon3bii ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0↔{B}\ne {0}_{ℎ}$
26 1 2 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
27 2 2 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
28 26 27 divclzi ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ$
29 25 28 sylbir ${⊢}{B}\ne {0}_{ℎ}\to \frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ$
30 oveq1 ${⊢}{x}=\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\to {x}{\cdot }_{ℎ}{B}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}$
31 30 rspceeqv ${⊢}\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\in ℂ\wedge {A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$
32 29 31 sylan ${⊢}\left({B}\ne {0}_{ℎ}\wedge {A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$
33 32 ex ${⊢}{B}\ne {0}_{ℎ}\to \left({A}=\left(\frac{{A}{\cdot }_{\mathrm{ih}}{B}}{{B}{\cdot }_{\mathrm{ih}}{B}}\right){\cdot }_{ℎ}{B}\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\right)$
34 22 33 sylbid ${⊢}{B}\ne {0}_{ℎ}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\right)$
35 21 34 pm2.61ine ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$
36 snssi ${⊢}{B}\in ℋ\to \left\{{B}\right\}\subseteq ℋ$
37 occl ${⊢}\left\{{B}\right\}\subseteq ℋ\to \perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
38 2 36 37 mp2b ${⊢}\perp \left(\left\{{B}\right\}\right)\in {\mathbf{C}}_{ℋ}$
39 38 choccli ${⊢}\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{C}}_{ℋ}$
40 39 chshii ${⊢}\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{S}}_{ℋ}$
41 h1did ${⊢}{B}\in ℋ\to {B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
42 2 41 ax-mp ${⊢}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
43 shmulcl ${⊢}\left(\perp \left(\perp \left(\left\{{B}\right\}\right)\right)\in {\mathbf{S}}_{ℋ}\wedge {x}\in ℂ\wedge {B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)\to {x}{\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
44 40 42 43 mp3an13 ${⊢}{x}\in ℂ\to {x}{\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
45 eleq1 ${⊢}{A}={x}{\cdot }_{ℎ}{B}\to \left({A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔{x}{\cdot }_{ℎ}{B}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
46 44 45 syl5ibrcom ${⊢}{x}\in ℂ\to \left({A}={x}{\cdot }_{ℎ}{B}\to {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)\right)$
47 46 rexlimiv ${⊢}\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}\to {A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)$
48 35 47 impbii ${⊢}{A}\in \perp \left(\perp \left(\left\{{B}\right\}\right)\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}={x}{\cdot }_{ℎ}{B}$