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 ∈ ℋ
h1de2.2 ⊢ B ∈ ℋ
Assertion h1de2ctlem ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 h1de2.1 ⊢ A ∈ ℋ
2 h1de2.2 ⊢ B ∈ ℋ
3 1 elexi ⊢ A ∈ V
4 3 elsn ⊢ A ∈ 0 ℎ ↔ A = 0 ℎ
5 hsn0elch ⊢ 0 ℎ ∈ C ℋ
6 5 ococi ⊢ ⊥ ⁡ ⊥ ⁡ 0 ℎ = 0 ℎ
7 6 eleq2i ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ 0 ℎ ↔ A ∈ 0 ℎ
8 ax-hvmul0 ⊢ B ∈ ℋ → 0 ⋅ ℎ B = 0 ℎ
9 2 8 ax-mp ⊢ 0 ⋅ ℎ B = 0 ℎ
10 9 eqeq2i ⊢ A = 0 ⋅ ℎ B ↔ A = 0 ℎ
11 4 7 10 3bitr4ri ⊢ A = 0 ⋅ ℎ B ↔ A ∈ ⊥ ⁡ ⊥ ⁡ 0 ℎ
12 sneq ⊢ B = 0 ℎ → B = 0 ℎ
13 12 fveq2d ⊢ B = 0 ℎ → ⊥ ⁡ B = ⊥ ⁡ 0 ℎ
14 13 fveq2d ⊢ B = 0 ℎ → ⊥ ⁡ ⊥ ⁡ B = ⊥ ⁡ ⊥ ⁡ 0 ℎ
15 14 eleq2d ⊢ B = 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ⊥ ⁡ ⊥ ⁡ 0 ℎ
16 11 15 bitr4id ⊢ B = 0 ℎ → A = 0 ⋅ ℎ B ↔ A ∈ ⊥ ⁡ ⊥ ⁡ B
17 0cn ⊢ 0 ∈ ℂ
18 oveq1 ⊢ x = 0 → x ⋅ ℎ B = 0 ⋅ ℎ B
19 18 rspceeqv ⊢ 0 ∈ ℂ ∧ A = 0 ⋅ ℎ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
20 17 19 mpan ⊢ A = 0 ⋅ ℎ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
21 16 20 syl6bir ⊢ B = 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
22 1 2 h1de2bi ⊢ B ≠ 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B
23 his6 ⊢ B ∈ ℋ → B ⋅ ih B = 0 ↔ B = 0 ℎ
24 2 23 ax-mp ⊢ B ⋅ ih B = 0 ↔ B = 0 ℎ
25 24 necon3bii ⊢ B ⋅ ih B ≠ 0 ↔ B ≠ 0 ℎ
26 1 2 hicli ⊢ A ⋅ ih B ∈ ℂ
27 2 2 hicli ⊢ B ⋅ ih B ∈ ℂ
28 26 27 divclzi ⊢ B ⋅ ih B ≠ 0 → A ⋅ ih B B ⋅ ih B ∈ ℂ
29 25 28 sylbir ⊢ B ≠ 0 ℎ → A ⋅ ih B B ⋅ ih B ∈ ℂ
30 oveq1 ⊢ x = A ⋅ ih B B ⋅ ih B → x ⋅ ℎ B = A ⋅ ih B B ⋅ ih B ⋅ ℎ B
31 30 rspceeqv ⊢ A ⋅ ih B B ⋅ ih B ∈ ℂ ∧ A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
32 29 31 sylan ⊢ B ≠ 0 ℎ ∧ A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
33 32 ex ⊢ B ≠ 0 ℎ → A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
34 22 33 sylbid ⊢ B ≠ 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
35 21 34 pm2.61ine ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → ∃ x ∈ ℂ A = x ⋅ ℎ B
36 snssi ⊢ B ∈ ℋ → B ⊆ ℋ
37 occl ⊢ B ⊆ ℋ → ⊥ ⁡ B ∈ C ℋ
38 2 36 37 mp2b ⊢ ⊥ ⁡ B ∈ C ℋ
39 38 choccli ⊢ ⊥ ⁡ ⊥ ⁡ B ∈ C ℋ
40 39 chshii ⊢ ⊥ ⁡ ⊥ ⁡ B ∈ S ℋ
41 h1did ⊢ B ∈ ℋ → B ∈ ⊥ ⁡ ⊥ ⁡ B
42 2 41 ax-mp ⊢ B ∈ ⊥ ⁡ ⊥ ⁡ B
43 shmulcl ⊢ ⊥ ⁡ ⊥ ⁡ B ∈ S ℋ ∧ x ∈ ℂ ∧ B ∈ ⊥ ⁡ ⊥ ⁡ B → x ⋅ ℎ B ∈ ⊥ ⁡ ⊥ ⁡ B
44 40 42 43 mp3an13 ⊢ x ∈ ℂ → x ⋅ ℎ B ∈ ⊥ ⁡ ⊥ ⁡ B
45 eleq1 ⊢ A = x ⋅ ℎ B → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ x ⋅ ℎ B ∈ ⊥ ⁡ ⊥ ⁡ B
46 44 45 syl5ibrcom ⊢ x ∈ ℂ → A = x ⋅ ℎ B → A ∈ ⊥ ⁡ ⊥ ⁡ B
47 46 rexlimiv ⊢ ∃ x ∈ ℂ A = x ⋅ ℎ B → A ∈ ⊥ ⁡ ⊥ ⁡ B
48 35 47 impbii ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B