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 biimtrrdi ⊢B=0ℎ→A∈⊥⁡⊥⁡B→∃x∈ℂA=x⋅ℎB
22 1 2 h1de2bi ⊢B≠0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB
23 his6 ⊢B∈ℋ→B⋅ihB=0↔B=0ℎ
24 2 23 ax-mp ⊢B⋅ihB=0↔B=0ℎ
25 24 necon3bii ⊢B⋅ihB≠0↔B≠0ℎ
26 1 2 hicli ⊢A⋅ihB∈ℂ
27 2 2 hicli ⊢B⋅ihB∈ℂ
28 26 27 divclzi ⊢B⋅ihB≠0→A⋅ihBB⋅ihB∈ℂ
29 25 28 sylbir ⊢B≠0ℎ→A⋅ihBB⋅ihB∈ℂ
30 oveq1 ⊢x=A⋅ihBB⋅ihB→x⋅ℎB=A⋅ihBB⋅ihB⋅ℎB
31 30 rspceeqv ⊢A⋅ihBB⋅ihB∈ℂ∧A=A⋅ihBB⋅ihB⋅ℎB→∃x∈ℂA=x⋅ℎB
32 29 31 sylan ⊢B≠0ℎ∧A=A⋅ihBB⋅ihB⋅ℎB→∃x∈ℂA=x⋅ℎB
33 32 ex ⊢B≠0ℎ→A=A⋅ihBB⋅ihB⋅ℎ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