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

Metamath Proof Explorer

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ℋ ) ) )