Theorem h1datomi

Description: A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h1datom.1	⊢ 𝐴 ∈ Cℋ
	h1datom.2	⊢ 𝐵 ∈ ℋ
Assertion	h1datomi	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		h1datom.1	⊢ 𝐴 ∈ Cℋ
2		h1datom.2	⊢ 𝐵 ∈ ℋ
3	1	chne0i	⊢ ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )
4		ssel	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
5	2	h1de2ci	⊢ ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) )
6		oveq1	⊢ ( 𝑦 = 0 → ( 𝑦 ·ℎ 𝐵 ) = ( 0 ·ℎ 𝐵 ) )
7		ax-hvmul0	⊢ ( 𝐵 ∈ ℋ → ( 0 ·ℎ 𝐵 ) = 0ℎ )
8	2 7	ax-mp	⊢ ( 0 ·ℎ 𝐵 ) = 0ℎ
9	6 8	eqtrdi	⊢ ( 𝑦 = 0 → ( 𝑦 ·ℎ 𝐵 ) = 0ℎ )
10		eqeq1	⊢ ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑥 = 0ℎ ↔ ( 𝑦 ·ℎ 𝐵 ) = 0ℎ ) )
11	9 10	imbitrrid	⊢ ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑦 = 0 → 𝑥 = 0ℎ ) )
12	11	necon3d	⊢ ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑥 ≠ 0ℎ → 𝑦 ≠ 0 ) )
13	12	adantl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑥 ≠ 0ℎ → 𝑦 ≠ 0 ) )
14		reccl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / 𝑦 ) ∈ ℂ )
15	1	chshii	⊢ 𝐴 ∈ Sℋ
16		shmulcl	⊢ ( ( 𝐴 ∈ Sℋ ∧ ( 1 / 𝑦 ) ∈ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 )
17	15 16	mp3an1	⊢ ( ( ( 1 / 𝑦 ) ∈ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 )
18	17	ex	⊢ ( ( 1 / 𝑦 ) ∈ ℂ → ( 𝑥 ∈ 𝐴 → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 ) )
19	14 18	syl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 ∈ 𝐴 → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 ) )
20	19	adantr	⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 ) )
21		oveq2	⊢ ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) = ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) )
22		simpl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → 𝑦 ∈ ℂ )
23		ax-hvmulass	⊢ ( ( ( 1 / 𝑦 ) ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( ( 1 / 𝑦 ) · 𝑦 ) ·ℎ 𝐵 ) = ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) )
24	2 23	mp3an3	⊢ ( ( ( 1 / 𝑦 ) ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 1 / 𝑦 ) · 𝑦 ) ·ℎ 𝐵 ) = ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) )
25	14 22 24	syl2anc	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( ( 1 / 𝑦 ) · 𝑦 ) ·ℎ 𝐵 ) = ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) )
26		recid2	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( 1 / 𝑦 ) · 𝑦 ) = 1 )
27	26	oveq1d	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( ( 1 / 𝑦 ) · 𝑦 ) ·ℎ 𝐵 ) = ( 1 ·ℎ 𝐵 ) )
28	25 27	eqtr3d	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) = ( 1 ·ℎ 𝐵 ) )
29		ax-hvmulid	⊢ ( 𝐵 ∈ ℋ → ( 1 ·ℎ 𝐵 ) = 𝐵 )
30	2 29	ax-mp	⊢ ( 1 ·ℎ 𝐵 ) = 𝐵
31	28 30	eqtrdi	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( 1 / 𝑦 ) ·ℎ ( 𝑦 ·ℎ 𝐵 ) ) = 𝐵 )
32	21 31	sylan9eqr	⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) = 𝐵 )
33	32	eleq1d	⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( ( ( 1 / 𝑦 ) ·ℎ 𝑥 ) ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
34	20 33	sylibd	⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
35	34	exp31	⊢ ( 𝑦 ∈ ℂ → ( 𝑦 ≠ 0 → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) ) ) )
36	35	com23	⊢ ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑦 ≠ 0 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) ) ) )
37	36	imp	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑦 ≠ 0 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) ) )
38	13 37	syld	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑥 ≠ 0ℎ → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) ) )
39	38	com3r	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ ℂ ∧ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) ) → ( 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) )
40	39	expd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ ℂ → ( 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) ) )
41	40	rexlimdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ 𝐵 ) → ( 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) )
42	5 41	biimtrid	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) )
43	4 42	sylcom	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) )
44	43	rexlimdv	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) )
45	3 44	biimtrid	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 ≠ 0ℋ → 𝐵 ∈ 𝐴 ) )
46		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
47		snssi	⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
48	2 47	ax-mp	⊢ { 𝐵 } ⊆ ℋ
49	1	chssii	⊢ 𝐴 ⊆ ℋ
50	48 49	occon2i	⊢ ( { 𝐵 } ⊆ 𝐴 → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
51	46 50	syl	⊢ ( 𝐵 ∈ 𝐴 → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
52	1	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
53	51 52	sseqtrdi	⊢ ( 𝐵 ∈ 𝐴 → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ 𝐴 )
54	45 53	syl6	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 ≠ 0ℋ → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ 𝐴 ) )
55	54	anc2li	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 ≠ 0ℋ → ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ 𝐴 ) ) )
56		eqss	⊢ ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ⊆ 𝐴 ) )
57	55 56	imbitrrdi	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 ≠ 0ℋ → 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
58	57	necon1d	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 ≠ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → 𝐴 = 0ℋ ) )
59		neor	⊢ ( ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) ↔ ( 𝐴 ≠ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → 𝐴 = 0ℋ ) )
60	58 59	sylibr	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) )