Theorem osumlem5 12207

Description: Lemma for osumi 12211.

Hypotheses

Ref	Expression
osumlem5.1	|- A e. CH
osumlem5.2	|- B e. CH

Assertion

Ref	Expression
osumlem5	|- (H:NN-->(A +H B) -> E.fE.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))))

Distinct variable groups:   w,f,g,A   w,B,f,g   w,H,f,g

Proof of Theorem osumlem5

Step	Hyp	Ref	Expression
1		ffvelrn 4916	. . . . 5 |- ((H:NN-->(A +H B) /\ w e. NN) -> (H` w) e. (A +H B))
2	1	ex 494	. . . 4 |- (H:NN-->(A +H B) -> (w e. NN -> (H` w) e. (A +H B)))
3		osumlem5.1	. . . . . 6 |- A e. CH
4	3	chshii 11722	. . . . 5 |- A e. SH
5		osumlem5.2	. . . . . 6 |- B e. CH
6	5	chshii 11722	. . . . 5 |- B e. SH
7	4, 6	shseli 11905	. . . 4 |- ((H` w) e. (A +H B) <-> E.x e. A E.y e. B (H` w) = (x +h y))
8	2, 7	syl6ib 282	. . 3 |- (H:NN-->(A +H B) -> (w e. NN -> E.x e. A E.y e. B (H` w) = (x +h y)))
9	8	r19.21aiv 2455	. 2 |- (H:NN-->(A +H B) -> A.w e. NN E.x e. A E.y e. B (H` w) = (x +h y))
10		nnex 7551	. . 3 |- NN e. _V
11	3	elisseti 2579	. . 3 |- A e. _V
12		opreq1 5025	. . . . 5 |- (x = (f` w) -> (x +h y) = ((f` w) +h y))
13	12	eqeq2d 2181	. . . 4 |- (x = (f` w) -> ((H` w) = (x +h y) <-> (H` w) = ((f` w) +h y)))
14	13	rexbidv 2404	. . 3 |- (x = (f` w) -> (E.y e. B (H` w) = (x +h y) <-> E.y e. B (H` w) = ((f` w) +h y)))
15	10, 11, 14	ac6 6396	. 2 |- (A.w e. NN E.x e. A E.y e. B (H` w) = (x +h y) -> E.f(f:NN-->A /\ A.w e. NN E.y e. B (H` w) = ((f` w) +h y)))
16	5	elisseti 2579	. . . . . 6 |- B e. _V
17		opreq2 5026	. . . . . . 7 |- (y = (g` w) -> ((f` w) +h y) = ((f` w) +h (g` w)))
18	17	eqeq2d 2181	. . . . . 6 |- (y = (g` w) -> ((H` w) = ((f` w) +h y) <-> (H` w) = ((f` w) +h (g` w))))
19	10, 16, 18	ac6 6396	. . . . 5 |- (A.w e. NN E.y e. B (H` w) = ((f` w) +h y) -> E.g(g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w))))
20	19	anim2i 635	. . . 4 |- ((f:NN-->A /\ A.w e. NN E.y e. B (H` w) = ((f` w) +h y)) -> (f:NN-->A /\ E.g(g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))))
21		anass 729	. . . . . 6 |- (((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))) <-> (f:NN-->A /\ (g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))))
22	21	exbii 1716	. . . . 5 |- (E.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))) <-> E.g(f:NN-->A /\ (g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))))
23		19.42v 1986	. . . . 5 |- (E.g(f:NN-->A /\ (g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))) <-> (f:NN-->A /\ E.g(g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))))
24	22, 23	bitri 306	. . . 4 |- (E.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))) <-> (f:NN-->A /\ E.g(g:NN-->B /\ A.w e. NN (H` w) = ((f` w) +h (g` w)))))
25	20, 24	sylibr 264	. . 3 |- ((f:NN-->A /\ A.w e. NN E.y e. B (H` w) = ((f` w) +h y)) -> E.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))))
26	25	eximi 1705	. 2 |- (E.f(f:NN-->A /\ A.w e. NN E.y e. B (H` w) = ((f` w) +h y)) -> E.fE.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))))
27	9, 15, 26	3syl 38	1 |- (H:NN-->(A +H B) -> E.fE.g((f:NN-->A /\ g:NN-->B) /\ A.w e. NN (H` w) = ((f` w) +h (g` w))))

Syntax hints:   -> wi 3   /\ wa 433   = wceq 1615   e. wcel 1617  E.wex 1644  A.wral 2385  E.wrex 2386  -->wf 4159  ` cfv 4163  (class class class)co 5020  NNcn 7094   +h cva 11417  CHcch 11426   +H cph 11428

This theorem is referenced by:  osumlem6 12208

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-ac 6385  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-i2m1 6897  ax-1ne0 6898  ax-rrecex 6901  ax-cnre 6902  ax-hilex 11497  ax-hfvadd 11498

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-int 3433  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-fv 4179  df-opr 5022  df-oprab 5023  df-n 7543  df-sh 11703  df-ch 11717  df-shsum 11898

Copyright terms: Public domain