This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℋ
h1de2.2 ⊢ 𝐵 ∈ ℋ
Assertion h1de2ctlem ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )

Proof

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