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 
|- ( ( B e. ~H /\ A =/= 0h ) -> ( A e. ( span ` { B } ) -> ( span ` { A } ) = ( span ` { B } ) ) )

Proof

Step Hyp Ref Expression
1 elspansn 
 |-  ( B e. ~H -> ( A e. ( span ` { B } ) <-> E. x e. CC A = ( x .h B ) ) )
2 1 adantr 
 |-  ( ( B e. ~H /\ A =/= 0h ) -> ( A e. ( span ` { B } ) <-> E. x e. CC A = ( x .h B ) ) )
3 sneq 
 |-  ( A = ( x .h B ) -> { A } = { ( x .h B ) } )
4 3 fveq2d 
 |-  ( A = ( x .h B ) -> ( span ` { A } ) = ( span ` { ( x .h B ) } ) )
5 4 ad2antll 
 |-  ( ( ( B e. ~H /\ A =/= 0h ) /\ ( x e. CC /\ A = ( x .h B ) ) ) -> ( span ` { A } ) = ( span ` { ( x .h B ) } ) )
6 oveq1 
 |-  ( x = 0 -> ( x .h B ) = ( 0 .h B ) )
7 ax-hvmul0 
 |-  ( B e. ~H -> ( 0 .h B ) = 0h )
8 6 7 sylan9eqr 
 |-  ( ( B e. ~H /\ x = 0 ) -> ( x .h B ) = 0h )
9 8 ex 
 |-  ( B e. ~H -> ( x = 0 -> ( x .h B ) = 0h ) )
10 eqeq1 
 |-  ( A = ( x .h B ) -> ( A = 0h <-> ( x .h B ) = 0h ) )
11 10 biimprd 
 |-  ( A = ( x .h B ) -> ( ( x .h B ) = 0h -> A = 0h ) )
12 9 11 sylan9 
 |-  ( ( B e. ~H /\ A = ( x .h B ) ) -> ( x = 0 -> A = 0h ) )
13 12 necon3d 
 |-  ( ( B e. ~H /\ A = ( x .h B ) ) -> ( A =/= 0h -> x =/= 0 ) )
14 13 ex 
 |-  ( B e. ~H -> ( A = ( x .h B ) -> ( A =/= 0h -> x =/= 0 ) ) )
15 14 com23 
 |-  ( B e. ~H -> ( A =/= 0h -> ( A = ( x .h B ) -> x =/= 0 ) ) )
16 15 impd 
 |-  ( B e. ~H -> ( ( A =/= 0h /\ A = ( x .h B ) ) -> x =/= 0 ) )
17 16 adantr 
 |-  ( ( B e. ~H /\ x e. CC ) -> ( ( A =/= 0h /\ A = ( x .h B ) ) -> x =/= 0 ) )
18 spansncol 
 |-  ( ( B e. ~H /\ x e. CC /\ x =/= 0 ) -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) )
19 18 3expia 
 |-  ( ( B e. ~H /\ x e. CC ) -> ( x =/= 0 -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) ) )
20 17 19 syld 
 |-  ( ( B e. ~H /\ x e. CC ) -> ( ( A =/= 0h /\ A = ( x .h B ) ) -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) ) )
21 20 exp4b 
 |-  ( B e. ~H -> ( x e. CC -> ( A =/= 0h -> ( A = ( x .h B ) -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) ) ) ) )
22 21 com23 
 |-  ( B e. ~H -> ( A =/= 0h -> ( x e. CC -> ( A = ( x .h B ) -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) ) ) ) )
23 22 imp43 
 |-  ( ( ( B e. ~H /\ A =/= 0h ) /\ ( x e. CC /\ A = ( x .h B ) ) ) -> ( span ` { ( x .h B ) } ) = ( span ` { B } ) )
24 5 23 eqtrd 
 |-  ( ( ( B e. ~H /\ A =/= 0h ) /\ ( x e. CC /\ A = ( x .h B ) ) ) -> ( span ` { A } ) = ( span ` { B } ) )
25 24 rexlimdvaa 
 |-  ( ( B e. ~H /\ A =/= 0h ) -> ( E. x e. CC A = ( x .h B ) -> ( span ` { A } ) = ( span ` { B } ) ) )
26 2 25 sylbid 
 |-  ( ( B e. ~H /\ A =/= 0h ) -> ( A e. ( span ` { B } ) -> ( span ` { A } ) = ( span ` { B } ) ) )