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 ⊢ A ∈ C ℋ ∧ B ∈ ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ B → A = ⊥ ⁡ ⊥ ⁡ B ∨ A = 0 ℋ

Proof

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