Theorem spanun 9405

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 9242	. . . . . . 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 9242	. . . . . . 7 |- (B (_ H~ -> (span` B) e. SH)
6	4, 5	ax-mp 7	. . . . . 6 |- (span` B) e. SH
7	3, 6	shscl 9219	. . . . 5 |- ((span` A) +H (span` B)) e. SH
8	7	shssi 9020	. . . 4 |- ((span` A) +H (span` B)) (_ H~
9		spanss2 9252	. . . . . . 7 |- (A (_ H~ -> A (_ (span` A))
10	1, 9	ax-mp 7	. . . . . 6 |- A (_ (span` A)
11		spanss2 9252	. . . . . . 7 |- (B (_ H~ -> B (_ (span` B))
12	4, 11	ax-mp 7	. . . . . 6 |- B (_ (span` B)
13		unss12 2198	. . . . . 6 |- ((A (_ (span` A) /\ B (_ (span` B)) -> (A u. B) (_ ((span` A) u. (span` B)))
14	10, 12, 13	mp2an 696	. . . . 5 |- (A u. B) (_ ((span` A) u. (span` B))
15	3, 6	shunss 9275	. . . . 5 |- ((span` A) u. (span` B)) (_ ((span` A) +H (span` B))
16	14, 15	sstri 2069	. . . 4 |- (A u. B) (_ ((span` A) +H (span` B))
17		spanss 9256	. . . 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 696	. . 3 |- (span` (A u. B)) (_ (span` ((span` A) +H (span` B)))
19		spanid 9255	. . . 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 2089	. 2 |- (span` (A u. B)) (_ ((span` A) +H (span` B))
22	3, 6	shsel 9218	. . . . 5 |- (x e. ((span` A) +H (span` B)) <-> E.z e. (span` A)E.w e. (span` B)x = (z +h w))
23		r2ex 1688	. . . . 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 1751	. . . . . . 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 1809	. . . . . . . . . . 11 |- z e. V
27	26	elspan 9404	. . . . . . . . . 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 1809	. . . . . . . . . . 11 |- w e. V
30	29	elspan 9404	. . . . . . . . . 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 1747	. . . . . . . 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 555	. . . . . . . . . . . . 13 |- (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) -> ((A (_ y /\ B (_ y) -> (z e. y /\ w e. y)))
37		unss 2200	. . . . . . . . . . . . 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 9025	. . . . . . . . . . . 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 1531	. . . . . . . . . . . 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 1701	. . . . . . 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 2201	. . . . . . . 8 |- (A u. B) (_ H~
48		visset 1809	. . . . . . . . 9 |- x e. V
49	48	elspan 9404	. . . . . . . 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 1294	. . . 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 2065	. 2 |- ((span` A) +H (span` B)) (_ (span` (A u. B))
56	21, 55	eqssi 2074	1 |- (span` (A u. B)) = ((span` A) +H (span` B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  A.wral 1642  E.wrex 1643   u. cun 2041   (_ wss 2043  ` cfv 3177  (class class class)co 3954  H~chil 8727   +h cva 8728  SHcsh 8736   +H cph 8739  spancspn 8740

This theorem is referenced by:  spanunt 9406  spanunsn 9442  spansnj 9531

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605  ax-hilex 8808  ax-hfvadd 8809  ax-hvcom 8810  ax-hvass 8811  ax-hv0cl 8812  ax-hvaddid 8813  ax-hfvmul 8814  ax-hvmulid 8815  ax-hvmulass 8816  ax-hvdistr1 8817  ax-hvdistr2 8818  ax-hvmul0 8819  ax-hfi 8885  ax-his1 8888  ax-his2 8889  ax-his3 8890  ax-his4 8891

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-nel 1585  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189