Theorem elspansn2t 9485

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

Proof of Theorem elspansn2t

Step	Hyp	Ref	Expression
1		spansnt 9477	. . . 4 |- (B e. H~ -> (span` {B}) = (_|_` (_|_` {B})))
2	1	eleq2d 1544	. . 3 |- (B e. H~ -> (A e. (span` {B}) <-> A e. (_|_` (_|_` {B}))))
3	2	3ad2ant2 803	. 2 |- ((A e. H~ /\ B e. H~ /\ B =/= 0h) -> (A e. (span` {B}) <-> A e. (_|_` (_|_` {B}))))
4		eleq1 1537	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (A e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) e. (_|_` (_|_` {B}))))
5		id 59	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> A = if(A e. H~, A, 0h))
6		opreq1 3974	. . . . . . . . 9 |- (A = if(A e. H~, A, 0h) -> (A .ih B) = (if(A e. H~, A, 0h) .ih B))
7	6	opreq1d 3981	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> ((A .ih B) / (B .ih B)) = ((if(A e. H~, A, 0h) .ih B) / (B .ih B)))
8	7	opreq1d 3981	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (((A .ih B) / (B .ih B)) .h B) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B))
9	5, 8	eqeq12d 1492	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (A = (((A .ih B) / (B .ih B)) .h B) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B)))
10	4, 9	bibi12d 631	. . . . 5 |- (A = if(A e. H~, A, 0h) -> ((A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B)) <-> (if(A e. H~, A, 0h) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B))))
11	10	imbi2d 614	. . . 4 |- (A = if(A e. H~, A, 0h) -> ((B =/= 0h -> (A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B))) <-> (B =/= 0h -> (if(A e. H~, A, 0h) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B)))))
12		neeq1 1593	. . . . 5 |- (B = if(B e. H~, B, 0h) -> (B =/= 0h <-> if(B e. H~, B, 0h) =/= 0h))
13		sneq 2421	. . . . . . . . 9 |- (B = if(B e. H~, B, 0h) -> {B} = {if(B e. H~, B, 0h)})
14	13	fveq2d 3734	. . . . . . . 8 |- (B = if(B e. H~, B, 0h) -> (_|_` {B}) = (_|_` {if(B e. H~, B, 0h)}))
15	14	fveq2d 3734	. . . . . . 7 |- (B = if(B e. H~, B, 0h) -> (_|_` (_|_` {B})) = (_|_` (_|_` {if(B e. H~, B, 0h)})))
16	15	eleq2d 1544	. . . . . 6 |- (B = if(B e. H~, B, 0h) -> (if(A e. H~, A, 0h) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) e. (_|_` (_|_` {if(B e. H~, B, 0h)}))))
17		opreq2 3975	. . . . . . . . 9 |- (B = if(B e. H~, B, 0h) -> (if(A e. H~, A, 0h) .ih B) = (if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)))
18		opreq1 3974	. . . . . . . . . 10 |- (B = if(B e. H~, B, 0h) -> (B .ih B) = (if(B e. H~, B, 0h) .ih B))
19		opreq2 3975	. . . . . . . . . 10 |- (B = if(B e. H~, B, 0h) -> (if(B e. H~, B, 0h) .ih B) = (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h)))
20	18, 19	eqtrd 1510	. . . . . . . . 9 |- (B = if(B e. H~, B, 0h) -> (B .ih B) = (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h)))
21	17, 20	opreq12d 3984	. . . . . . . 8 |- (B = if(B e. H~, B, 0h) -> ((if(A e. H~, A, 0h) .ih B) / (B .ih B)) = ((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))))
22		id 59	. . . . . . . 8 |- (B = if(B e. H~, B, 0h) -> B = if(B e. H~, B, 0h))
23	21, 22	opreq12d 3984	. . . . . . 7 |- (B = if(B e. H~, B, 0h) -> (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B) = (((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))) .h if(B e. H~, B, 0h)))
24	23	eqeq2d 1489	. . . . . 6 |- (B = if(B e. H~, B, 0h) -> (if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))) .h if(B e. H~, B, 0h))))
25	16, 24	bibi12d 631	. . . . 5 |- (B = if(B e. H~, B, 0h) -> ((if(A e. H~, A, 0h) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B)) <-> (if(A e. H~, A, 0h) e. (_|_` (_|_` {if(B e. H~, B, 0h)})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))) .h if(B e. H~, B, 0h)))))
26	12, 25	imbi12d 628	. . . 4 |- (B = if(B e. H~, B, 0h) -> ((B =/= 0h -> (if(A e. H~, A, 0h) e. (_|_` (_|_` {B})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih B) / (B .ih B)) .h B))) <-> (if(B e. H~, B, 0h) =/= 0h -> (if(A e. H~, A, 0h) e. (_|_` (_|_` {if(B e. H~, B, 0h)})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))) .h if(B e. H~, B, 0h))))))
27		ax-hv0cl 8868	. . . . . 6 |- 0h e. H~
28	27	elimel 2398	. . . . 5 |- if(A e. H~, A, 0h) e. H~
29	27	elimel 2398	. . . . 5 |- if(B e. H~, B, 0h) e. H~
30	28, 29	h1de2b 9472	. . . 4 |- (if(B e. H~, B, 0h) =/= 0h -> (if(A e. H~, A, 0h) e. (_|_` (_|_` {if(B e. H~, B, 0h)})) <-> if(A e. H~, A, 0h) = (((if(A e. H~, A, 0h) .ih if(B e. H~, B, 0h)) / (if(B e. H~, B, 0h) .ih if(B e. H~, B, 0h))) .h if(B e. H~, B, 0h))))
31	11, 26, 30	dedth2h 2391	. . 3 |- ((A e. H~ /\ B e. H~) -> (B =/= 0h -> (A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B))))
32	31	3impia 832	. 2 |- ((A e. H~ /\ B e. H~ /\ B =/= 0h) -> (A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B)))
33	3, 32	bitrd