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
spansnm0.2 B
Assertion spansnm0i ¬ A span B span A span B = 0

Proof

Step Hyp Ref Expression
1 spansnm0.1 A
2 spansnm0.2 B
3 2 spansnchi span B C
4 3 chshii span B S
5 elspansn5 span B S A ¬ A span B x span A x span B x = 0
6 4 5 ax-mp A ¬ A span B x span A x span B x = 0
7 1 6 mpanl1 ¬ A span B x span A x span B x = 0
8 7 ex ¬ A span B x span A x span B x = 0
9 elin x span A span B x span A x span B
10 elch0 x 0 x = 0
11 8 9 10 3imtr4g ¬ A span B x span A span B x 0
12 11 ssrdv ¬ A span B span A span B 0
13 1 spansnchi span A C
14 13 3 chincli span A span B C
15 14 chle0i span A span B 0 span A span B = 0
16 12 15 sylib ¬ A span B span A span B = 0