Theorem spansneleq

Description: Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansneleq	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		elspansn	⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
2	1	adantr	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
3		sneq	⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → { 𝐴 } = { ( 𝑥 ·ℎ 𝐵 ) } )
4	3	fveq2d	⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( span ‘ { 𝐴 } ) = ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) )
5	4	ad2antll	⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) ) → ( span ‘ { 𝐴 } ) = ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) )
6		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ·ℎ 𝐵 ) = ( 0 ·ℎ 𝐵 ) )
7		ax-hvmul0	⊢ ( 𝐵 ∈ ℋ → ( 0 ·ℎ 𝐵 ) = 0ℎ )
8	6 7	sylan9eqr	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 = 0 ) → ( 𝑥 ·ℎ 𝐵 ) = 0ℎ )
9	8	ex	⊢ ( 𝐵 ∈ ℋ → ( 𝑥 = 0 → ( 𝑥 ·ℎ 𝐵 ) = 0ℎ ) )
10		eqeq1	⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( 𝐴 = 0ℎ ↔ ( 𝑥 ·ℎ 𝐵 ) = 0ℎ ) )
11	10	biimprd	⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( ( 𝑥 ·ℎ 𝐵 ) = 0ℎ → 𝐴 = 0ℎ ) )
12	9 11	sylan9	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( 𝑥 = 0 → 𝐴 = 0ℎ ) )
13	12	necon3d	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( 𝐴 ≠ 0ℎ → 𝑥 ≠ 0 ) )
14	13	ex	⊢ ( 𝐵 ∈ ℋ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( 𝐴 ≠ 0ℎ → 𝑥 ≠ 0 ) ) )
15	14	com23	⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ≠ 0ℎ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → 𝑥 ≠ 0 ) ) )
16	15	impd	⊢ ( 𝐵 ∈ ℋ → ( ( 𝐴 ≠ 0ℎ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → 𝑥 ≠ 0 ) )
17	16	adantr	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ≠ 0ℎ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → 𝑥 ≠ 0 ) )
18		spansncol	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) )
19	18	3expia	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ≠ 0 → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) ) )
20	17 19	syld	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ≠ 0ℎ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) ) )
21	20	exp4b	⊢ ( 𝐵 ∈ ℋ → ( 𝑥 ∈ ℂ → ( 𝐴 ≠ 0ℎ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) ) ) ) )
22	21	com23	⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ≠ 0ℎ → ( 𝑥 ∈ ℂ → ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) ) ) ) )
23	22	imp43	⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) ) → ( span ‘ { ( 𝑥 ·ℎ 𝐵 ) } ) = ( span ‘ { 𝐵 } ) )
24	5 23	eqtrd	⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) ) → ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) )
25	24	rexlimdvaa	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) ) )
26	2 25	sylbid	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) ) )