Theorem spansncv 9597

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 323	. 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 9485	. . . 4 |- (span` {C}) e. CH
5		spansncv.2	. . . 4 |- B e. CH
6	2, 4, 5	chlubi 9395	. . 3 |- ((A (_ B /\ (span` {C}) (_ B) -> (A vH (span` {C})) (_ B)
7		pssss 2143	. . . 4 |- (A (. B -> A (_ B)
8	7	adantr 389	. . 3 |- ((A (. B /\ B (_ (A vH (span` {C}))) -> A (_ B)
9		ssel2 2064	. . . . . . . . . . . . 13 |- ((B (_ (A vH (span` {C})) /\ x e. B) -> x e. (A vH (span` {C})))
10	2, 3	spansnj 9591	. . . . . . . . . . . . . . . 16 |- (A +H (span` {C})) = (A vH (span` {C}))
11	10	eleq2i 1538	. . . . . . . . . . . . . . 15 |- (x e. (A +H (span` {C})) <-> x e. (A vH (span` {C})))
12	2, 4	chsel 9382	. . . . . . . . . . . . . . 15 |- (x e. (A +H (span` {C})) <-> E.y e. A E.z e. (span` {C})x = (y +h z))
13	11, 12	bitr3 175	. . . . . . . . . . . . . 14 |- (x e. (A vH (span` {C})) <-> E.y e. A E.z e. (span` {C})x = (y +h z))
14		hvpncan2t 8909	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. H~ /\ z e. H~) -> ((y +h z) -h y) = z)
15	2	chel 9102	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. A -> y e. H~)
16	4	chel 9102	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. (span` {C}) -> z e. H~)
17	14, 15, 16	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ z e. (span` {C})) -> ((y +h z) -h y) = z)
18	17	eleq1d 1540	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. A /\ z e. (span` {C})) -> (((y +h z) -h y) e. B <-> z e. B))
19	5	chshi 9097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- B e. SH
20		shsubcltOLD 9090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (B e. SH -> (((y +h z) e. B /\ y e. B) -> ((y +h z) -h y) e. B))
21	19, 20	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y +h z) e. B /\ y e. B) -> ((y +h z) -h y) e. B)
22		eleq1 1534	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = (y +h z) -> (x e. B <-> (y +h z) e. B))
23	22	biimpac 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. B /\ x = (y +h z)) -> (y +h z) e. B)
24		ssel2 2064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A (_ B /\ y e. A) -> y e. B)
25	24, 7	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A (. B /\ y e. A) -> y e. B)
26	21, 23, 25	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((x e. B /\ x = (y +h z)) /\ (A (. B /\ y e. A)) -> ((y +h z) -h y) e. B)
27	26	exp43 384	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. B -> (x = (y +h z) -> (A (. B -> (y e. A -> ((y +h z) -h y) e. B))))
28	27	com14 38	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. A -> (x = (y +h z) -> (A (. B -> (x e. B -> ((y +h z) -h y) e. B))))
29	28	imp45 372	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. A /\ (x = (y +h z) /\ (A (. B /\ x e. B))) -> ((y +h z) -h y) e. B)
30	18, 29	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. A /\ z e. (span` {C})) -> ((y e. A /\ (x = (y +h z) /\ (A (. B /\ x e. B))) -> z e. B))
31	30	imp 350	. . . . . . . . . . . . . . . . . . . . 21 |- (((y e. A /\ z e. (span` {C})) /\ (y e. A /\ (x = (y +h z) /\ (A (. B /\ x e. B)))) -> z e. B)
32	31	anandis 512	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. A /\ (z e. (span` {C}) /\ (x = (y +h z) /\ (A (. B /\ x e. B)))) -> z e. B)
33	32	exp45 386	. . . . . . . . . . . . . . . . . . 19 |- (y e. A -> (z e. (span` {C}) -> (x = (y +h z) -> ((A (. B /\ x e. B) -> z e. B))))
34	33	imp41 368	. . . . . . . . . . . . . . . . . 18 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +h z)) /\ (A (. B /\ x e. B)) -> z e. B)
35	34	adantrr 395	. . . . . . . . . . . . . . . . 17 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +h z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> z e. B)
36		spansneleq 9493	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((C e. H~ /\ z =/= 0h) -> (z e. (span` {C}) -> (span` {z}) = (span` {C})))
37	3, 36	mpan 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z =/= 0h -> (z e. (span` {C}) -> (span` {z}) = (span` {C})))
38	37	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z =/= 0h /\ z e. (span` {C})) -> (span` {z}) = (span` {C}))
39	38	sseq1d 2088	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z =/= 0h /\ z e. (span` {C})) -> ((span` {z}) (_ B <-> (span` {C}) (_ B))
40		spansnsst 9494	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. SH /\ z e. B) -> (span` {z}) (_ B)
41	19, 40	mpan 695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. B -> (span` {z}) (_ B)
42	39, 41	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z =/= 0h /\ z e. (span` {C})) -> (z e. B -> (span` {C}) (_ B))
43	42	ancoms 436	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. (span` {C}) /\ z =/= 0h) -> (z e. B -> (span` {C}) (_ B))
44		opreq2 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = 0h -> (y +h z) = (y +h 0h))
45		ax-hvaddid 8874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y e. H~ -> (y +h 0h) = y)
46	15, 45	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. A -> (y +h 0h) = y)
47	44, 46	sylan9eqr 1529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. A /\ z = 0h) -> (y +h z) = y)
48	47	eqeq2d 1486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. A /\ z = 0h) -> (x = (y +h z) <-> x = y))
49		eleq1a 1543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. A -> (x = y -> x e. A))
50	49	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. A /\ z = 0h) -> (x = y -> x e. A))
51	48, 50	sylbid 203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. A /\ z = 0h) -> (x = (y +h z) -> x e. A))
52	51	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. A -> (z = 0h -> (x = (y +h z) -> x e. A)))
53	52	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. A -> (x = (y +h z) -> (z = 0h -> x e. A)))
54	53	imp 350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. A /\ x = (y +h z)) -> (z = 0h -> x e. A))
55	54	necon3bd 1603	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. A /\ x = (y +h z)) -> (-. x e. A -> z =/= 0h))
56	55	imp 350	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. A /\ x = (y +h z)) /\ -. x e. A) -> z =/= 0h)
57	43, 56	sylan2 451	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. (span` {C}) /\ ((y e. A /\ x = (y +h z)) /\ -. x e. A)) -> (z e. B -> (span` {C}) (_ B))
58	57	exp44 385	. . . . . . . . . . . . . . . . . . . 20 |- (z e. (span` {C}) -> (y e. A -> (x = (y +h z) -> (-. x e. A -> (z e. B -> (span` {C}) (_ B)))))
59	58	com12 11	. . . . . . . . . . . . . . . . . . 19 |- (y e. A -> (z e. (span` {C}) -> (x = (y +h z) -> (-. x e. A -> (z e. B -> (span` {C}) (_ B)))))
60	59	imp41 368	. . . . . . . . . . . . . . . . . 18 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +h z)) /\ -. x e. A) -> (z e. B -> (span` {C}) (_ B))
61	60	adantrl 394	. . . . . . . . . . . . . . . . 17 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +h z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> (z e. B -> (span` {C}) (_ B))
62	35, 61	mpd 26	. . . . . . . . . . . . . . . 16 |- ((((y e. A /\ z e. (span` {C})) /\ x = (y +h z)) /\ ((A (. B /\ x e. B) /\ -. x e. A)) -> (span` {C}) (_ B)
63	62	exp43 384	. . . . . . . . . . . . . . 15 |- ((y e. A /\ z e. (span` {C})) -> (x = (y +h z) -> ((A (. B /\ x e. B) -> (-. x e. A -> (span` {C}) (_ B))