Theorem elspansn2t 5472

Description: Membership in the span of a singleton. All members are collinear with the generating vector.

Assertion

Ref	Expression
elspansn2t	|- ((A e. H~ /\ B e. H~ /\ -. B = 0v) -> (A e. (span` {B}) <-> A = (((A .i B) / (B .i B)) .s B)))

Proof of Theorem elspansn2t

Step	Hyp	Ref	Expression
1		spansnt 5464	. . . . 5 |- (B e. H~ -> (span` {B}) = (_|_` (_|_` {B})))
2	1	eleq2d 1156	. . . 4 |- (B e. H~ -> (A e. (span` {B}) <-> A e. (_|_` (_|_` {B}))))
3	2	adantl 305	. . 3 |- ((A e. H~ /\ B e. H~) -> (A e. (span` {B}) <-> A e. (_|_` (_|_` {B}))))
4	3	3adant3 599	. 2 |- ((A e. H~ /\ B e. H~ /\ -. B = 0v) -> (A e. (span` {B}) <-> A e. (_|_` (_|_` {B}))))
5		eleq1 1149	. . . . . . 7 |- (A = if(A e. H~, A, 0v) -> (A e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) e. (_|_` (_|_` {B}))))
6		id 9	. . . . . . . 8 |- (A = if(A e. H~, A, 0v) -> A = if(A e. H~, A, 0v))
7		opreq1 3006	. . . . . . . . . 10 |- (A = if(A e. H~, A, 0v) -> (A .i B) = (if(A e. H~, A, 0v) .i B))
8	7	opreq1d 3012	. . . . . . . . 9 |- (A = if(A e. H~, A, 0v) -> ((A .i B) / (B .i B)) = ((if(A e. H~, A, 0v) .i B) / (B .i B)))
9	8	opreq1d 3012	. . . . . . . 8 |- (A = if(A e. H~, A, 0v) -> (((A .i B) / (B .i B)) .s B) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B))
10	6, 9	cleq12d 1115	. . . . . . 7 |- (A = if(A e. H~, A, 0v) -> (A = (((A .i B) / (B .i B)) .s B) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B)))
11	5, 10	bibi12d 477	. . . . . 6 |- (A = if(A e. H~, A, 0v) -> ((A e. (_|_` (_|_` {B})) <-> A = (((A .i B) / (B .i B)) .s B)) <-> (if(A e. H~, A, 0v) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B))))
12	11	imbi2d 464	. . . . 5 |- (A = if(A e. H~, A, 0v) -> ((-. B = 0v -> (A e. (_|_` (_|_` {B})) <-> A = (((A .i B) / (B .i B)) .s B))) <-> (-. B = 0v -> (if(A e. H~, A, 0v) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B)))))
13		cleq1 1107	. . . . . . 7 |- (B = if(B e. H~, B, 0v) -> (B = 0v <-> if(B e. H~, B, 0v) = 0v))
14	13	negbid 463	. . . . . 6 |- (B = if(B e. H~, B, 0v) -> (-. B = 0v <-> -. if(B e. H~, B, 0v) = 0v))
15		sneq 1816	. . . . . . . . . 10 |- (B = if(B e. H~, B, 0v) -> {B} = {if(B e. H~, B, 0v)})
16	15	fveq2d 2836	. . . . . . . . 9 |- (B = if(B e. H~, B, 0v) -> (_|_` {B}) = (_|_` {if(B e. H~, B, 0v)}))
17	16	fveq2d 2836	. . . . . . . 8 |- (B = if(B e. H~, B, 0v) -> (_|_` (_|_` {B})) = (_|_` (_|_` {if(B e. H~, B, 0v)})))
18	17	eleq2d 1156	. . . . . . 7 |- (B = if(B e. H~, B, 0v) -> (if(A e. H~, A, 0v) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) e. (_|_` (_|_` {if(B e. H~, B, 0v)}))))
19		opreq2 3007	. . . . . . . . . 10 |- (B = if(B e. H~, B, 0v) -> (if(A e. H~, A, 0v) .i B) = (if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)))
20		opreq1 3006	. . . . . . . . . . 11 |- (B = if(B e. H~, B, 0v) -> (B .i B) = (if(B e. H~, B, 0v) .i B))
21		opreq2 3007	. . . . . . . . . . 11 |- (B = if(B e. H~, B, 0v) -> (if(B e. H~, B, 0v) .i B) = (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v)))
22	20, 21	eqtrd 1128	. . . . . . . . . 10 |- (B = if(B e. H~, B, 0v) -> (B .i B) = (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v)))
23	19, 22	opreq12d 3014	. . . . . . . . 9 |- (B = if(B e. H~, B, 0v) -> ((if(A e. H~, A, 0v) .i B) / (B .i B)) = ((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))))
24		id 9	. . . . . . . . 9 |- (B = if(B e. H~, B, 0v) -> B = if(B e. H~, B, 0v))
25	23, 24	opreq12d 3014	. . . . . . . 8 |- (B = if(B e. H~, B, 0v) -> (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B) = (((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))) .s if(B e. H~, B, 0v)))
26	25	cleq2d 1112	. . . . . . 7 |- (B = if(B e. H~, B, 0v) -> (if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))) .s if(B e. H~, B, 0v))))
27	18, 26	bibi12d 477	. . . . . 6 |- (B = if(B e. H~, B, 0v) -> ((if(A e. H~, A, 0v) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B)) <-> (if(A e. H~, A, 0v) e. (_|_` (_|_` {if(B e. H~, B, 0v)})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))) .s if(B e. H~, B, 0v)))))
28	14, 27	imbi12d 474	. . . . 5 |- (B = if(B e. H~, B, 0v) -> ((-. B = 0v -> (if(A e. H~, A, 0v) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i B) / (B .i B)) .s B))) <-> (-. if(B e. H~, B, 0v) = 0v -> (if(A e. H~, A, 0v) e. (_|_` (_|_` {if(B e. H~, B, 0v)})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))) .s if(B e. H~, B, 0v))))))
29		ax-hvzercl 4987	. . . . . . 7 |- 0v e. H~
30	29	elimel 1793	. . . . . 6 |- if(A e. H~, A, 0v) e. H~
31	29	elimel 1793	. . . . . 6 |- if(B e. H~, B, 0v) e. H~
32	30, 31	h1de2b 5459	. . . . 5 |- (-. if(B e. H~, B, 0v) = 0v -> (if(A e. H~, A, 0v) e. (_|_` (_|_` {if(B e. H~, B, 0v)})) <-> if(A e. H~, A, 0v) = (((if(A e. H~, A, 0v) .i if(B e. H~, B, 0v)) / (if(B e. H~, B, 0v) .i if(B e. H~, B, 0v))) .s if(B e. H~, B, 0v))))
33	12, 28, 32	dedth2h 1787	. . . 4 |- ((A e. H~ /\ B e. H~) -> (-. B = 0v -> (A e. (_|_` (_|_` {B})) <-> A = (((A .i B) / (B .i B)) .s B))))
34	33	imp 277	. . 3 |- (((A e. H~