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

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 ⊢ 𝐴 ∈ Cℋ
h1datom.2 ⊢ 𝐵 ∈ ℋ
Assertion h1datomi ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐴 = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∨ 𝐴 = 0ℋ ) )

Proof

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