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