Theorem spansncol 5473

Description: The singletons of collinear vectors have the same span.

Assertion

Ref	Expression
spansncol	|- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (span` {(B .s A)}) = (span` {A}))

Proof of Theorem spansncol

Step	Hyp	Ref	Expression
1		axmulcl 4068	. . . . . . . . . . . 12 |- ((y e. CC /\ B e. CC) -> (y x. B) e. CC)
2	1	ancoms 334	. . . . . . . . . . 11 |- ((B e. CC /\ y e. CC) -> (y x. B) e. CC)
3	2	adantll 309	. . . . . . . . . 10 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (y x. B) e. CC)
4	3	a1d 14	. . . . . . . . 9 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (x = (y .s (B .s A)) -> (y x. B) e. CC))
5		ax-hvmulass 4992	. . . . . . . . . . . . 13 |- ((y e. CC /\ B e. CC /\ A e. H~) -> ((y x. B) .s A) = (y .s (B .s A)))
6	5	3com13 615	. . . . . . . . . . . 12 |- ((A e. H~ /\ B e. CC /\ y e. CC) -> ((y x. B) .s A) = (y .s (B .s A)))
7	6	3expa 612	. . . . . . . . . . 11 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> ((y x. B) .s A) = (y .s (B .s A)))
8	7	cleq2d 1112	. . . . . . . . . 10 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (x = ((y x. B) .s A) <-> x = (y .s (B .s A))))
9	8	biimprd 136	. . . . . . . . 9 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (x = (y .s (B .s A)) -> x = ((y x. B) .s A)))
10	4, 9	jcad 455	. . . . . . . 8 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (x = (y .s (B .s A)) -> ((y x. B) e. CC /\ x = ((y x. B) .s A))))
11		opreq1 3006	. . . . . . . . . 10 |- (z = (y x. B) -> (z .s A) = ((y x. B) .s A))
12	11	cleq2d 1112	. . . . . . . . 9 |- (z = (y x. B) -> (x = (z .s A) <-> x = ((y x. B) .s A)))
13	12	rcla4ev 1403	. . . . . . . 8 |- (((y x. B) e. CC /\ x = ((y x. B) .s A)) -> E.z e. CC x = (z .s A))
14	10, 13	syl6 23	. . . . . . 7 |- (((A e. H~ /\ B e. CC) /\ y e. CC) -> (x = (y .s (B .s A)) -> E.z e. CC x = (z .s A)))
15	14	exp 291	. . . . . 6 |- ((A e. H~ /\ B e. CC) -> (y e. CC -> (x = (y .s (B .s A)) -> E.z e. CC x = (z .s A))))
16	15	r19.23adv 1286	. . . . 5 |- ((A e. H~ /\ B e. CC) -> (E.y e. CC x = (y .s (B .s A)) -> E.z e. CC x = (z .s A)))
17	16	3adant3 599	. . . 4 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (E.y e. CC x = (y .s (B .s A)) -> E.z e. CC x = (z .s A)))
18		divclt 4223	. . . . . . . . . . . . 13 |- (((z e. CC /\ B e. CC) /\ B =/= 0) -> (z / B) e. CC)
19	18	anasss 337	. . . . . . . . . . . 12 |- ((z e. CC /\ (B e. CC /\ B =/= 0)) -> (z / B) e. CC)
20	19	adantlr 310	. . . . . . . . . . 11 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (z / B) e. CC)
21	20	a1d 14	. . . . . . . . . 10 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (x = (z .s A) -> (z / B) e. CC))
22		ax-hvmulass 4992	. . . . . . . . . . . . . 14 |- (((z / B) e. CC /\ B e. CC /\ A e. H~) -> (((z / B) x. B) .s A) = ((z / B) .s (B .s A)))
23		pm3.26 256	. . . . . . . . . . . . . . 15 |- ((B e. CC /\ B =/= 0) -> B e. CC)
24	23	adantl 305	. . . . . . . . . . . . . 14 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> B e. CC)
25		pm3.27 260	. . . . . . . . . . . . . . 15 |- ((z e. CC /\ A e. H~) -> A e. H~)
26	25	adantr 306	. . . . . . . . . . . . . 14 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> A e. H~)
27	22, 20, 24, 26	syl3anc 629	. . . . . . . . . . . . 13 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (((z / B) x. B) .s A) = ((z / B) .s (B .s A)))
28		divcan1t 4228	. . . . . . . . . . . . . . . . . 18 |- (((B e. CC /\ z e. CC) /\ B =/= 0) -> ((z / B) x. B) = z)
29	28	exp31 293	. . . . . . . . . . . . . . . . 17 |- (B e. CC -> (z e. CC -> (B =/= 0 -> ((z / B) x. B) = z)))
30	29	com12 13	. . . . . . . . . . . . . . . 16 |- (z e. CC -> (B e. CC -> (B =/= 0 -> ((z / B) x. B) = z)))
31	30	imp32 281	. . . . . . . . . . . . . . 15 |- ((z e. CC /\ (B e. CC /\ B =/= 0)) -> ((z / B) x. B) = z)
32	31	adantlr 310	. . . . . . . . . . . . . 14 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> ((z / B) x. B) = z)
33	32	opreq1d 3012	. . . . . . . . . . . . 13 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (((z / B) x. B) .s A) = (z .s A))
34	27, 33	eqtr3d 1130	. . . . . . . . . . . 12 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> ((z / B) .s (B .s A)) = (z .s A))
35	34	cleq2d 1112	. . . . . . . . . . 11 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (x = ((z / B) .s (B .s A)) <-> x = (z .s A)))
36	35	biimprd 136	. . . . . . . . . 10 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (x = (z .s A) -> x = ((z / B) .s (B .s A))))
37	21, 36	jcad 455	. . . . . . . . 9 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (x = (z .s A) -> ((z / B) e. CC /\ x = ((z / B) .s (B .s A)))))
38		opreq1 3006	. . . . . . . . . . 11 |- (y = (z / B) -> (y .s (B .s A)) = ((z / B) .s (B .s A)))
39	38	cleq2d 1112	. . . . . . . . . 10 |- (y = (z / B) -> (x = (y .s (B .s A)) <-> x = ((z / B) .s (B .s A))))
40	39	rcla4ev 1403	. . . . . . . . 9 |- (((z / B) e. CC /\ x = ((z / B) .s (B .s A))) -> E.y e. CC x = (y .s (B .s A)))
41	37, 40	syl6 23	. . . . . . . 8 |- (((z e. CC /\ A e. H~) /\ (B e. CC /\ B =/= 0)) -> (x = (z .s A) -> E.y e. CC x = (y .s (B .s A))))
42	41	exp43 301	. . . . . . 7 |- (z e. CC -> (A e. H~ -> (B e. CC -> (B =/= 0 -> (x = (z .s A) -> E.y e. CC x = (y .s (B .s A)))))))
43	42	com4l 39	. . . . . 6 |- (A e. H~ -> (B e. CC -> (B =/= 0 -> (z e. CC -> (x = (z .s A) -> E.y e. CC x = (y .s (B .s A)))))))
44	43	3imp 608	. . . . 5 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (z e. CC -> (x = (z .s A) -> E.y e. CC x = (y .s (B .s A)))))
45	44	r19.23adv 1286	. . . 4 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (E.z e. CC x = (z .s A) -> E.y e. CC x = (y .s (B .s A))))
46	17, 45	impbid 397	. . 3 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (E.y e. CC x = (y .s (B .s A)) <-> E.z e. CC x = (z .s A)))
47		ax-hvmulcl 4989	. . . . . 6 |- ((B e. CC /\ A e. H~) -> (B .s A) e. H~)
48	47	ancoms 334	. . . . 5 |- ((A e. H~ /\ B e. CC) -> (B .s A) e. H~)
49		elspansnt 5471	. . . . 5 |- ((B .s A) e. H~ -> (x e. (span` {(B .s A)}) <-> E.y e. CC x = (y .s (B .s A))))
50	48, 49	syl 12	. . . 4 |- ((A e. H~ /\ B e. CC) -> (x e. (span` {(B .s A)}) <-> E.y e. CC x = (y .s (B .s A))))
51	50	3adant3 599	. . 3 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (x e. (span` {(B .s A)}) <-> E.y e. CC x = (y .s (B .s A))))
52		elspansnt 5471	. . . . 5 |- (A e. H~ -> (x e. (span` {A}) <-> E.z e. CC x = (z .s A)))
53	52	adantr 306	. . . 4 |- ((A e. H~ /\ B e. CC) -> (x e. (span` {A}) <-> E.z e. CC x = (z .s A)))
54	53	3adant3 599	. . 3 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (x e. (span` {A}) <-> E.z e. CC x = (z .s A)))
55	46, 51, 54	3bitr4d 424	. 2 |- ((A e. H~ /\ B e. CC /\ B =/= 0) -> (x e. (span` {(B