Theorem spansncv 5542

Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153.

Hypotheses

Ref	Expression
spansncv.1	|- A e. CH
spansncv.2	|- B e. CH
spansncv.3	|- C e. H~

Assertion

Ref	Expression
spansncv	|- ((A (. B /\ B (_ (A vH (span` {C}))) -> B = (A vH (span` {C})))

Proof of Theorem spansncv

Step	Hyp	Ref	Expression
1		pm3.27 260	. 2 |- ((A (. B /\ B (_ (A vH (span` {C}))) -> B (_ (A vH (span` {C})))
2		spansncv.1	. . . 4 |- A e. CH
3		spansncv.3	. . . . 5 |- C e. H~
4	3	spansnch 5467	. . . 4 |- (span` {C}) e. CH
5		spansncv.2	. . . 4 |- B e. CH
6	2, 4, 5	chlubi 5393	. . 3 |- ((A (_ B /\ (span` {C}) (_ B) -> (A vH (span` {C})) (_ B)
7		pssss 1567	. . . 4 |- (A (. B -> A (_ B)
8	7	adantr 306	. . 3 |- ((A (. B /\ B (_ (A vH (span` {C}))) -> A (_ B)
9		ssel2 1503	. . . . . . . . . . . . . 14 |- ((B (_ (A vH (span` {C})) /\ x e. B) -> x e. (A vH (span` {C})))
10	2, 3	spansnj 5539	. . . . . . . . . . . . . . . . 17 |- (A +H (span` {C})) = (A vH (span` {C}))
11	10	eleq2i 1153	. . . . . . . . . . . . . . . 16 |- (x e. (A +H (span` {C})) <-> x e. (A vH (span` {C})))
12	2, 4	chsel 5381	. . . . . . . . . . . . . . . 16 |- (x e. (A +H (span` {C})) <-> E.y e. A E.z e. (span` {C})x = (y +v z))
13	11, 12	bitr3 153	. . . . . . . . . . . . . . 15 |- (x e. (A vH (span` {C})) <-> E.y e. A E.z e. (span` {C})x = (y +v z))
14		hvsubcan2t 5017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ z e. H~) -> ((y +v z) -v y) = z)
15	2	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. A -> y e. H~)
16	4	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. (span` {C}) -> z e. H~)
17	14, 15, 16	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ z e. (span` {C})) -> ((y +v z) -v y) = z)
18	17	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ z e. (span` {C})) -> (((y +v z) -v y) e. B <-> z e. B))
19	5	chshi 5132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- B e. SH
20		shsubclt 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (B e. SH -> (((y +v z) e. B /\ y e. B) -> ((y +v z) -v y) e. B))
21	19, 20	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y +v z) e. B /\ y e. B) -> ((y +v z) -v y) e. B)
22		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (y +v z) -> (x e. B <-> (y +v z) e. B))
23	22	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x e. B /\ x = (y +v z)) -> (y +v z) e. B)
24		ssel2 1503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A (_ B /\ y e. A) -> y e. B)
25	24, 7	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A (. B /\ y e. A) -> y e. B)
26	21, 23, 25	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((x e. B /\ x = (y +v z)) /\ (A (. B /\ y e. A)) -> ((y +v z) -v y) e. B)
27	26	exp43 301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. B -> (x = (y +v z) -> (A (. B -> (y e. A -> ((y +v z) -v y) e. B))))
28	27	com14 38	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. A -> (x = (y +v z) -> (A (. B -> (x e. B -> ((y +v z) -v y) e. B))))
29	28	imp45 290	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ (x = (y +v z) /\ (A (. B /\ x e. B))) -> ((y +v z) -v y) e. B)
30	18, 29	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. A /\ z e. (span` {C})) -> ((y e. A /\ (x = (y +v z) /\ (A (. B /\ x e. B))) -> z e. B))
31	30	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. A /\ z e. (span` {C})) /\ (y e. A /\ (x = (y +v z) /\ (A (. B /\ x e. B)))) -> z e. B)
32	31	anandis 394	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. A /\ (z e. (span` {C}) /\ (x = (y +v z) /\ (A (. B /\ x e. B)))) -> z e. B)
33	32	exp45 303	. . . . . . . . . . . . . . . . . . . 20 |- (y e. A -> (z e. (span` {C}) -> (x = (y +v z) -> ((A (. B /\ x e. B) -> z e. B))))
34	33	imp41 286	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +v z)) /\ (A (. B /\ x e. B)) -> z e. B)
35	34	adantrr 312	. . . . . . . . . . . . . . . . . 18 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +v z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> z e. B)
36		spansneleq 5475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((C e. H~ /\ -. z = 0v) -> (z e. (span` {C}) -> (span` {z}) = (span` {C})))
37	3, 36	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (-. z = 0v -> (z e. (span` {C}) -> (span` {z}) = (span` {C})))
38	37	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((-. z = 0v /\ z e. (span` {C})) -> (span` {z}) = (span` {C}))
39	38	sseq1d 1527	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((-. z = 0v /\ z e. (span` {C})) -> ((span` {z}) (_ B <-> (span` {C}) (_ B))
40		spansnsst 5476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. SH /\ z e. B) -> (span` {z}) (_ B)
41	19, 40	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. B -> (span` {z}) (_ B)
42	39, 41	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((-. z = 0v /\ z e. (span` {C})) -> (z e. B -> (span` {C}) (_ B))
43	42	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. (span` {C}) /\ -. z = 0v) -> (z e. B -> (span` {C}) (_ B))
44		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = 0v -> (y +v z) = (y +v 0v))
45		ax-hvaddid 4988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y e. H~ -> (y +v 0v) = y)
46	15, 45	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y e. A -> (y +v 0v) = y)
47	44, 46	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y e. A /\ z = 0v) -> (y +v z) = y)
48	47	cleq2d 1112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. A /\ z = 0v) -> (x = (y +v z) <-> x = y))
49		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. A -> (x = y -> x e. A))
50	49	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. A /\ z = 0v) -> (x = y -> x e. A))
51	48, 50	sylbid 178	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. A /\ z = 0v) -> (x = (y +v z) -> x e. A))
52	51	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. A -> (z = 0v -> (x = (y +v z) -> x e. A)))
53	52	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. A -> (x = (y +v z) -> (z = 0v -> x e. A)))
54	53	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. A /\ x = (y +v z)) -> (z = 0v -> x e. A))
55	54	con3d 87	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ x = (y +v z)) -> (-. x e. A -> -. z = 0v))
56	55	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y e. A /\ x = (y +v z)) /\ -. x e. A) -> -. z = 0v)
57	43, 56	sylan2 346	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. (span` {C}) /\ ((y e. A /\ x = (y +v z)) /\ -. x e. A)) -> (z e. B -> (span` {C}) (_ B))
58	57	exp44 302	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. (span` {C}) -> (y e. A -> (x = (y +v z) -> (-. x e. A -> (z e. B -> (span` {C}) (_ B)))))
59	58	com12 13	. . . . . . . . . . . . . . . . . . . 20 |- (y e. A -> (z e. (span` {C}) -> (x = (y +v z) -> (-. x e. A -> (z e. B -> (span` {C}) (_ B)))))
60	59	imp41 286	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +v z)) /\ -. x e. A) -> (z e. B -> (span` {C}) (_ B))
61	60	adantrl 311	. . . . . . . . . . . . . . . . . 18 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +v z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> (z e. B -> (span` {C}) (_ B))
62	35, 61	mpd 46	. . . . . . . . . . . . . . . . 17 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +v z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> (span` {C}) (_ B)
63	62	exp43 301	. . . . . . . . . . . . . . . 16 |- ((y e. A /\ z e. (span` {C})) -> (x = (y +v z) -> ((A (. B /\ x e. B) -> (-. x e. A -> (span` {C}) (_ B))))
64	63	r19.23aivv 1287	. . . . . . . . . . . . . . 15 |- (E.y e. A E.z e. (span` {C})x = (y +v z) -> ((A (. B /\ x e. B) -> (-. x e. A -> (span` {C})