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 )