Theorem spanun 9467

Description: The span of a union is the subspace sum of spans.

Hypotheses

Ref	Expression
spanun.1	|- A (_ H~
spanun.2	|- B (_ H~

Assertion

Ref	Expression
spanun	|- (span` (A u. B)) = ((span` A) +H (span` B))

Proof of Theorem spanun

Step	Hyp	Ref	Expression
1		spanun.1	. . . . . . 7 |- A (_ H~
2		spanclt 9304	. . . . . . 7 |- (A (_ H~ -> (span` A) e. SH)
3	1, 2	ax-mp 7	. . . . . 6 |- (span` A) e. SH
4		spanun.2	. . . . . . 7 |- B (_ H~
5		spanclt 9304	. . . . . . 7 |- (B (_ H~ -> (span` B) e. SH)
6	4, 5	ax-mp 7	. . . . . 6 |- (span` B) e. SH
7	3, 6	shscl 9281	. . . . 5 |- ((span` A) +H (span` B)) e. SH
8	7	shssi 9081	. . . 4 |- ((span` A) +H (span` B)) (_ H~
9		spanss2 9314	. . . . . . 7 |- (A (_ H~ -> A (_ (span` A))
10	1, 9	ax-mp 7	. . . . . 6 |- A (_ (span` A)
11		spanss2 9314	. . . . . . 7 |- (B (_ H~ -> B (_ (span` B))
12	4, 11	ax-mp 7	. . . . . 6 |- B (_ (span` B)
13		unss12 2202	. . . . . 6 |- ((A (_ (span` A) /\ B (_ (span` B)) -> (A u. B) (_ ((span` A) u. (span` B)))
14	10, 12, 13	mp2an 697	. . . . 5 |- (A u. B) (_ ((span` A) u. (span` B))
15	3, 6	shunss 9337	. . . . 5 |- ((span` A) u. (span` B)) (_ ((span` A) +H (span` B))
16	14, 15	sstri 2073	. . . 4 |- (A u. B) (_ ((span` A) +H (span` B))
17		spanss 9318	. . . 4 |- ((((span` A) +H (span` B)) (_ H~ /\ (A u. B) (_ ((span` A) +H (span` B))) -> (span` (A u. B)) (_ (span` ((span` A) +H (span` B))))
18	8, 16, 17	mp2an 697	. . 3 |- (span` (A u. B)) (_ (span` ((span` A) +H (span` B)))
19		spanid 9317	. . . 4 |- (((span` A) +H (span` B)) e. SH -> (span` ((span` A) +H (span` B))) = ((span` A) +H (span` B)))
20	7, 19	ax-mp 7	. . 3 |- (span` ((span` A) +H (span` B))) = ((span` A) +H (span` B))
21	18, 20	sseqtr 2093	. 2 |- (span` (A u. B)) (_ ((span` A) +H (span` B))
22	3, 6	shsel 9280	. . . . 5 |- (x e. ((span` A) +H (span` B)) <-> E.z e. (span` A)E.w e. (span` B)x = (z +h w))
23		r2ex 1691	. . . . 5 |- (E.z e. (span` A)E.w e. (span` B)x = (z +h w) <-> E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)))
24	22, 23	bitr 173	. . . 4 |- (x e. ((span` A) +H (span` B)) <-> E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)))
25		r19.27av 1754	. . . . . . 7 |- ((A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)))
26		visset 1813	. . . . . . . . . . 11 |- z e. V
27	26	elspan 9466	. . . . . . . . . 10 |- (A (_ H~ -> (z e. (span` A) <-> A.y e. SH (A (_ y -> z e. y)))
28	1, 27	ax-mp 7	. . . . . . . . 9 |- (z e. (span` A) <-> A.y e. SH (A (_ y -> z e. y))
29		visset 1813	. . . . . . . . . . 11 |- w e. V
30	29	elspan 9466	. . . . . . . . . 10 |- (B (_ H~ -> (w e. (span` B) <-> A.y e. SH (B (_ y -> w e. y)))
31	4, 30	ax-mp 7	. . . . . . . . 9 |- (w e. (span` B) <-> A.y e. SH (B (_ y -> w e. y))
32	28, 31	anbi12i 482	. . . . . . . 8 |- ((z e. (span` A) /\ w e. (span` B)) <-> (A.y e. SH (A (_ y -> z e. y) /\ A.y e. SH (B (_ y -> w e. y)))
33		r19.26 1750	. . . . . . . 8 |- (A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) <-> (A.y e. SH (A (_ y -> z e. y) /\ A.y e. SH (B (_ y -> w e. y)))
34	32, 33	bitr4 176	. . . . . . 7 |- ((z e. (span` A) /\ w e. (span` B)) <-> A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)))
35	25, 34	sylanb 449	. . . . . 6 |- (((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)))
36		prth 556	. . . . . . . . . . . . 13 |- (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) -> ((A (_ y /\ B (_ y) -> (z e. y /\ w e. y)))
37		unss 2204	. . . . . . . . . . . . 13 |- ((A (_ y /\ B (_ y) <-> (A u. B) (_ y)
38	36, 37	syl5ibr 207	. . . . . . . . . . . 12 |- (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) -> ((A u. B) (_ y -> (z e. y /\ w e. y)))
39		shaddcltOLD 9086	. . . . . . . . . . . 12 |- (y e. SH -> ((z e. y /\ w e. y) -> (z +h w) e. y))
40	38, 39	sylan9r 469	. . . . . . . . . . 11 |- ((y e. SH /\ ((A (_ y -> z e. y) /\ (B (_ y -> w e. y))) -> ((A u. B) (_ y -> (z +h w) e. y))
41		eleq1 1534	. . . . . . . . . . . 12 |- (x = (z +h w) -> (x e. y <-> (z +h w) e. y))
42	41	biimprd 154	. . . . . . . . . . 11 |- (x = (z +h w) -> ((z +h w) e. y -> x e. y))
43	40, 42	sylan9 468	. . . . . . . . . 10 |- (((y e. SH /\ ((A (_ y -> z e. y) /\ (B (_ y -> w e. y))) /\ x = (z +h w)) -> ((A u. B) (_ y -> x e. y))
44	43	exp42 383	. . . . . . . . 9 |- (y e. SH -> ((A (_ y -> z e. y) -> ((B (_ y -> w e. y) -> (x = (z +h w) -> ((A u. B) (_ y -> x e. y)))))
45	44	imp4c 366	. . . . . . . 8 |- (y e. SH -> ((((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> ((A u. B) (_ y -> x e. y)))
46	45	r19.20i 1704	. . . . . . 7 |- (A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> A.y e. SH ((A u. B) (_ y -> x e. y))
47	1, 4	unssi 2205	. . . . . . . 8 |- (A u. B) (_ H~
48		visset 1813	. . . . . . . . 9 |- x e. V
49	48	elspan 9466	. . . . . . . 8 |- ((A u. B) (_ H~ -> (x e. (span` (A u. B)) <-> A.y e. SH ((A u. B) (_ y -> x e. y)))
50	47, 49	ax-mp 7	. . . . . . 7 |- (x e. (span` (A u. B)) <-> A.y e. SH ((A u. B) (_ y -> x e. y))
51	46, 50	sylibr 200	. . . . . 6 |- (A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
52	35, 51	syl 10	. . . . 5 |- (((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
53	52	19.23aivv 1296	. . . 4 |- (E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
54	24, 53	sylbi 199	. . 3 |- (x e. ((span` A) +H (span` B)) -> x e. (span` (A u. B)))
55	54	ssriv 2069	. 2 |- ((span` A) +H (span` B)) (_ (span` (A u. B))
56	21, 55	eqssi 2078	1 |- (span` (A u. B)) = ((span` A) +H (span` B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  A.wral 1645  E.wrex 1646   u. cun 2045   (_ wss 2047  ` cfv 3182  (class class class)co 3963  H~chil 8788   +h cva 8789  SHcsh 8797   +H cph 8800  spancspn 8801

This theorem is referenced by:  spanunt 9468  spanunsn 9502  spansnj 9591

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625  ax-hilex 8869  ax-hfvadd 8870  ax-hvcom 8871  ax-hvass 8872  ax-hv0cl 8873  ax-hvaddid 8874  ax-hfvmul 8875  ax-hvmulid 8876  ax-hvmulass 8877  ax-hvdistr1 8878  ax-hvdistr2 8879  ax-hvmul0 8880  ax-hfi 8946  ax-his1 8949  ax-his2 8950  ax-his3 8951  ax-his4 8952

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-nel 1588  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-pss 2055  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-iun 2568  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952  df-lim 2953  df-suc 2954  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193