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∈Ax≠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 imbitrrid ⊢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→1y∈ℂ
15 1 chshii ⊢A∈Sℋ
16 shmulcl ⊢A∈Sℋ∧1y∈ℂ∧x∈A→1y⋅ℎx∈A
17 15 16 mp3an1 ⊢1y∈ℂ∧x∈A→1y⋅ℎx∈A
18 17 ex ⊢1y∈ℂ→x∈A→1y⋅ℎx∈A
19 14 18 syl ⊢y∈ℂ∧y≠0→x∈A→1y⋅ℎx∈A
20 19 adantr ⊢y∈ℂ∧y≠0∧x=y⋅ℎB→x∈A→1y⋅ℎx∈A
21 oveq2 ⊢x=y⋅ℎB→1y⋅ℎx=1y⋅ℎy⋅ℎB
22 simpl ⊢y∈ℂ∧y≠0→y∈ℂ
23 ax-hvmulass ⊢1y∈ℂ∧y∈ℂ∧B∈ℋ→1y⁢y⋅ℎB=1y⋅ℎy⋅ℎB
24 2 23 mp3an3 ⊢1y∈ℂ∧y∈ℂ→1y⁢y⋅ℎB=1y⋅ℎy⋅ℎB
25 14 22 24 syl2anc ⊢y∈ℂ∧y≠0→1y⁢y⋅ℎB=1y⋅ℎy⋅ℎB
26 recid2 ⊢y∈ℂ∧y≠0→1y⁢y=1
27 26 oveq1d ⊢y∈ℂ∧y≠0→1y⁢y⋅ℎB=1⋅ℎB
28 25 27 eqtr3d ⊢y∈ℂ∧y≠0→1y⋅ℎ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→1y⋅ℎy⋅ℎB=B
32 21 31 sylan9eqr ⊢y∈ℂ∧y≠0∧x=y⋅ℎB→1y⋅ℎx=B
33 32 eleq1d ⊢y∈ℂ∧y≠0∧x=y⋅ℎB→1y⋅ℎ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 biimtrid ⊢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∈Ax≠0ℎ→B∈A
45 3 44 biimtrid ⊢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ℋ