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 ⊢B∈ℋ∧A≠0ℎ→A∈span⁡B→span⁡A=span⁡B

Proof

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