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

Metamath Proof Explorer

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 ‘ { 𝐵 } ) ) )