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=ifA∈CℋA0ℋ→A⊆⊥⁡⊥⁡B↔ifA∈CℋA0ℋ⊆⊥⁡⊥⁡B
2 eqeq1 ⊢A=ifA∈CℋA0ℋ→A=⊥⁡⊥⁡B↔ifA∈CℋA0ℋ=⊥⁡⊥⁡B
3 eqeq1 ⊢A=ifA∈CℋA0ℋ→A=0ℋ↔ifA∈CℋA0ℋ=0ℋ
4 2 3 orbi12d ⊢A=ifA∈CℋA0ℋ→A=⊥⁡⊥⁡B∨A=0ℋ↔ifA∈CℋA0ℋ=⊥⁡⊥⁡B∨ifA∈CℋA0ℋ=0ℋ
5 1 4 imbi12d ⊢A=ifA∈CℋA0ℋ→A⊆⊥⁡⊥⁡B→A=⊥⁡⊥⁡B∨A=0ℋ↔ifA∈CℋA0ℋ⊆⊥⁡⊥⁡B→ifA∈CℋA0ℋ=⊥⁡⊥⁡B∨ifA∈CℋA0ℋ=0ℋ
6 sneq ⊢B=ifB∈ℋB0ℎ→B=ifB∈ℋB0ℎ
7 6 fveq2d ⊢B=ifB∈ℋB0ℎ→⊥⁡B=⊥⁡ifB∈ℋB0ℎ
8 7 fveq2d ⊢B=ifB∈ℋB0ℎ→⊥⁡⊥⁡B=⊥⁡⊥⁡ifB∈ℋB0ℎ
9 8 sseq2d ⊢B=ifB∈ℋB0ℎ→ifA∈CℋA0ℋ⊆⊥⁡⊥⁡B↔ifA∈CℋA0ℋ⊆⊥⁡⊥⁡ifB∈ℋB0ℎ
10 8 eqeq2d ⊢B=ifB∈ℋB0ℎ→ifA∈CℋA0ℋ=⊥⁡⊥⁡B↔ifA∈CℋA0ℋ=⊥⁡⊥⁡ifB∈ℋB0ℎ
11 10 orbi1d ⊢B=ifB∈ℋB0ℎ→ifA∈CℋA0ℋ=⊥⁡⊥⁡B∨ifA∈CℋA0ℋ=0ℋ↔ifA∈CℋA0ℋ=⊥⁡⊥⁡ifB∈ℋB0ℎ∨ifA∈CℋA0ℋ=0ℋ
12 9 11 imbi12d ⊢B=ifB∈ℋB0ℎ→ifA∈CℋA0ℋ⊆⊥⁡⊥⁡B→ifA∈CℋA0ℋ=⊥⁡⊥⁡B∨ifA∈CℋA0ℋ=0ℋ↔ifA∈CℋA0ℋ⊆⊥⁡⊥⁡ifB∈ℋB0ℎ→ifA∈CℋA0ℋ=⊥⁡⊥⁡ifB∈ℋB0ℎ∨ifA∈CℋA0ℋ=0ℋ
13 h0elch ⊢0ℋ∈Cℋ
14 13 elimel ⊢ifA∈CℋA0ℋ∈Cℋ
15 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
16 14 15 h1datomi ⊢ifA∈CℋA0ℋ⊆⊥⁡⊥⁡ifB∈ℋB0ℎ→ifA∈CℋA0ℋ=⊥⁡⊥⁡ifB∈ℋB0ℎ∨ifA∈CℋA0ℋ=0ℋ
17 5 12 16 dedth2h ⊢A∈Cℋ∧B∈ℋ→A⊆⊥⁡⊥⁡B→A=⊥⁡⊥⁡B∨A=0ℋ