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	⊢ 𝐴 ∈ ℋ
	spansnm0.2	⊢ 𝐵 ∈ ℋ
Assertion	spansnm0i	⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		spansnm0.1	⊢ 𝐴 ∈ ℋ
2		spansnm0.2	⊢ 𝐵 ∈ ℋ
3	2	spansnchi	⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ
4	3	chshii	⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
5		elspansn5	⊢ ( ( span ‘ { 𝐵 } ) ∈ Sℋ → ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ ) )
6	4 5	ax-mp	⊢ ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ )
7	1 6	mpanl1	⊢ ( ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ )
8	7	ex	⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) → 𝑥 = 0ℎ ) )
9		elin	⊢ ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ↔ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) )
10		elch0	⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ )
11	8 9 10	3imtr4g	⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) → 𝑥 ∈ 0ℋ ) )
12	11	ssrdv	⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ )
13	1	spansnchi	⊢ ( span ‘ { 𝐴 } ) ∈ Cℋ
14	13 3	chincli	⊢ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ∈ Cℋ
15	14	chle0i	⊢ ( ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ ↔ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )
16	12 15	sylib	⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ )