Theorem h1datom

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

	Ref	Expression
Assertion	h1datom	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
2		eqeq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
3		eqeq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 = 0ℋ ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) )
4	2 3	orbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ) )
5	1 4	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ) ) )
6		sneq	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → { 𝐵 } = { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } )
7	6	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ⊥ ‘ { 𝐵 } ) = ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) )
8	7	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) )
9	8	sseq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ) )
10	8	eqeq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ) )
11	10	orbi1d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ) )
12	9 11	imbi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) ) ) )
13		h0elch	⊢ 0ℋ ∈ Cℋ
14	13	elimel	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
15		ifhvhv0	⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
16	14 15	h1datomi	⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ∨ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) = 0ℋ ) )
17	5 12 16	dedth2h	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) ) )