Metamath Proof Explorer

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 ⊢ A ∈ C ℋ
h1datom.2 ⊢ B ∈ ℋ
Assertion h1datomi ⊢ A ⊆ ⊥ ⁡ ⊥ ⁡ B → A = ⊥ ⁡ ⊥ ⁡ B ∨ A = 0 ℋ

Proof

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