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 e. CH
h1datom.2 
|- B e. ~H
Assertion h1datomi 
|- ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) )

Proof

Step Hyp Ref Expression
1 h1datom.1 
 |-  A e. CH
2 h1datom.2 
 |-  B e. ~H
3 1 chne0i 
 |-  ( A =/= 0H <-> E. x e. A x =/= 0h )
4 ssel 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( x e. A -> x e. ( _|_ ` ( _|_ ` { B } ) ) ) )
5 2 h1de2ci 
 |-  ( x e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. y e. CC x = ( y .h B ) )
6 oveq1 
 |-  ( y = 0 -> ( y .h B ) = ( 0 .h B ) )
7 ax-hvmul0 
 |-  ( B e. ~H -> ( 0 .h B ) = 0h )
8 2 7 ax-mp 
 |-  ( 0 .h B ) = 0h
9 6 8 eqtrdi 
 |-  ( y = 0 -> ( y .h B ) = 0h )
10 eqeq1 
 |-  ( x = ( y .h B ) -> ( x = 0h <-> ( y .h B ) = 0h ) )
11 9 10 imbitrrid 
 |-  ( x = ( y .h B ) -> ( y = 0 -> x = 0h ) )
12 11 necon3d 
 |-  ( x = ( y .h B ) -> ( x =/= 0h -> y =/= 0 ) )
13 12 adantl 
 |-  ( ( y e. CC /\ x = ( y .h B ) ) -> ( x =/= 0h -> y =/= 0 ) )
14 reccl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( 1 / y ) e. CC )
15 1 chshii 
 |-  A e. SH
16 shmulcl 
 |-  ( ( A e. SH /\ ( 1 / y ) e. CC /\ x e. A ) -> ( ( 1 / y ) .h x ) e. A )
17 15 16 mp3an1 
 |-  ( ( ( 1 / y ) e. CC /\ x e. A ) -> ( ( 1 / y ) .h x ) e. A )
18 17 ex 
 |-  ( ( 1 / y ) e. CC -> ( x e. A -> ( ( 1 / y ) .h x ) e. A ) )
19 14 18 syl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( x e. A -> ( ( 1 / y ) .h x ) e. A ) )
20 19 adantr 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ x = ( y .h B ) ) -> ( x e. A -> ( ( 1 / y ) .h x ) e. A ) )
21 oveq2 
 |-  ( x = ( y .h B ) -> ( ( 1 / y ) .h x ) = ( ( 1 / y ) .h ( y .h B ) ) )
22 simpl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> y e. CC )
23 ax-hvmulass 
 |-  ( ( ( 1 / y ) e. CC /\ y e. CC /\ B e. ~H ) -> ( ( ( 1 / y ) x. y ) .h B ) = ( ( 1 / y ) .h ( y .h B ) ) )
24 2 23 mp3an3 
 |-  ( ( ( 1 / y ) e. CC /\ y e. CC ) -> ( ( ( 1 / y ) x. y ) .h B ) = ( ( 1 / y ) .h ( y .h B ) ) )
25 14 22 24 syl2anc 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( ( 1 / y ) x. y ) .h B ) = ( ( 1 / y ) .h ( y .h B ) ) )
26 recid2 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( 1 / y ) x. y ) = 1 )
27 26 oveq1d 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( ( 1 / y ) x. y ) .h B ) = ( 1 .h B ) )
28 25 27 eqtr3d 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( 1 / y ) .h ( y .h B ) ) = ( 1 .h B ) )
29 ax-hvmulid 
 |-  ( B e. ~H -> ( 1 .h B ) = B )
30 2 29 ax-mp 
 |-  ( 1 .h B ) = B
31 28 30 eqtrdi 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( 1 / y ) .h ( y .h B ) ) = B )
32 21 31 sylan9eqr 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ x = ( y .h B ) ) -> ( ( 1 / y ) .h x ) = B )
33 32 eleq1d 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ x = ( y .h B ) ) -> ( ( ( 1 / y ) .h x ) e. A <-> B e. A ) )
34 20 33 sylibd 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ x = ( y .h B ) ) -> ( x e. A -> B e. A ) )
35 34 exp31 
 |-  ( y e. CC -> ( y =/= 0 -> ( x = ( y .h B ) -> ( x e. A -> B e. A ) ) ) )
36 35 com23 
 |-  ( y e. CC -> ( x = ( y .h B ) -> ( y =/= 0 -> ( x e. A -> B e. A ) ) ) )
37 36 imp 
 |-  ( ( y e. CC /\ x = ( y .h B ) ) -> ( y =/= 0 -> ( x e. A -> B e. A ) ) )
38 13 37 syld 
 |-  ( ( y e. CC /\ x = ( y .h B ) ) -> ( x =/= 0h -> ( x e. A -> B e. A ) ) )
39 38 com3r 
 |-  ( x e. A -> ( ( y e. CC /\ x = ( y .h B ) ) -> ( x =/= 0h -> B e. A ) ) )
40 39 expd 
 |-  ( x e. A -> ( y e. CC -> ( x = ( y .h B ) -> ( x =/= 0h -> B e. A ) ) ) )
41 40 rexlimdv 
 |-  ( x e. A -> ( E. y e. CC x = ( y .h B ) -> ( x =/= 0h -> B e. A ) ) )
42 5 41 biimtrid 
 |-  ( x e. A -> ( x e. ( _|_ ` ( _|_ ` { B } ) ) -> ( x =/= 0h -> B e. A ) ) )
43 4 42 sylcom 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( x e. A -> ( x =/= 0h -> B e. A ) ) )
44 43 rexlimdv 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( E. x e. A x =/= 0h -> B e. A ) )
45 3 44 biimtrid 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A =/= 0H -> B e. A ) )
46 snssi 
 |-  ( B e. A -> { B } C_ A )
47 snssi 
 |-  ( B e. ~H -> { B } C_ ~H )
48 2 47 ax-mp 
 |-  { B } C_ ~H
49 1 chssii 
 |-  A C_ ~H
50 48 49 occon2i 
 |-  ( { B } C_ A -> ( _|_ ` ( _|_ ` { B } ) ) C_ ( _|_ ` ( _|_ ` A ) ) )
51 46 50 syl 
 |-  ( B e. A -> ( _|_ ` ( _|_ ` { B } ) ) C_ ( _|_ ` ( _|_ ` A ) ) )
52 1 ococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
53 51 52 sseqtrdi 
 |-  ( B e. A -> ( _|_ ` ( _|_ ` { B } ) ) C_ A )
54 45 53 syl6 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A =/= 0H -> ( _|_ ` ( _|_ ` { B } ) ) C_ A ) )
55 54 anc2li 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A =/= 0H -> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) /\ ( _|_ ` ( _|_ ` { B } ) ) C_ A ) ) )
56 eqss 
 |-  ( A = ( _|_ ` ( _|_ ` { B } ) ) <-> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) /\ ( _|_ ` ( _|_ ` { B } ) ) C_ A ) )
57 55 56 imbitrrdi 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A =/= 0H -> A = ( _|_ ` ( _|_ ` { B } ) ) ) )
58 57 necon1d 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A =/= ( _|_ ` ( _|_ ` { B } ) ) -> A = 0H ) )
59 neor 
 |-  ( ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) <-> ( A =/= ( _|_ ` ( _|_ ` { B } ) ) -> A = 0H ) )
60 58 59 sylibr 
 |-  ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) )