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

Metamath Proof Explorer

Theorem spansnm0i

Description: The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

Ref Expression
Hypotheses spansnm0.1 
|- A e. ~H
spansnm0.2 
|- B e. ~H
Assertion spansnm0i 
|- ( -. A e. ( span ` { B } ) -> ( ( span ` { A } ) i^i ( span ` { B } ) ) = 0H )

Proof

Step Hyp Ref Expression
1 spansnm0.1 
 |-  A e. ~H
2 spansnm0.2 
 |-  B e. ~H
3 2 spansnchi 
 |-  ( span ` { B } ) e. CH
4 3 chshii 
 |-  ( span ` { B } ) e. SH
5 elspansn5 
 |-  ( ( span ` { B } ) e. SH -> ( ( ( A e. ~H /\ -. A e. ( span ` { B } ) ) /\ ( x e. ( span ` { A } ) /\ x e. ( span ` { B } ) ) ) -> x = 0h ) )
6 4 5 ax-mp 
 |-  ( ( ( A e. ~H /\ -. A e. ( span ` { B } ) ) /\ ( x e. ( span ` { A } ) /\ x e. ( span ` { B } ) ) ) -> x = 0h )
7 1 6 mpanl1 
 |-  ( ( -. A e. ( span ` { B } ) /\ ( x e. ( span ` { A } ) /\ x e. ( span ` { B } ) ) ) -> x = 0h )
8 7 ex 
 |-  ( -. A e. ( span ` { B } ) -> ( ( x e. ( span ` { A } ) /\ x e. ( span ` { B } ) ) -> x = 0h ) )
9 elin 
 |-  ( x e. ( ( span ` { A } ) i^i ( span ` { B } ) ) <-> ( x e. ( span ` { A } ) /\ x e. ( span ` { B } ) ) )
10 elch0 
 |-  ( x e. 0H <-> x = 0h )
11 8 9 10 3imtr4g 
 |-  ( -. A e. ( span ` { B } ) -> ( x e. ( ( span ` { A } ) i^i ( span ` { B } ) ) -> x e. 0H ) )
12 11 ssrdv 
 |-  ( -. A e. ( span ` { B } ) -> ( ( span ` { A } ) i^i ( span ` { B } ) ) C_ 0H )
13 1 spansnchi 
 |-  ( span ` { A } ) e. CH
14 13 3 chincli 
 |-  ( ( span ` { A } ) i^i ( span ` { B } ) ) e. CH
15 14 chle0i 
 |-  ( ( ( span ` { A } ) i^i ( span ` { B } ) ) C_ 0H <-> ( ( span ` { A } ) i^i ( span ` { B } ) ) = 0H )
16 12 15 sylib 
 |-  ( -. A e. ( span ` { B } ) -> ( ( span ` { A } ) i^i ( span ` { B } ) ) = 0H )