Theorem ovnsubadd2lem

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnsubadd2lem.x	|- ( ph -> X e. Fin )
	ovnsubadd2lem.a	|- ( ph -> A C_ ( RR ^m X ) )
	ovnsubadd2lem.b	|- ( ph -> B C_ ( RR ^m X ) )
	ovnsubadd2lem.c	|- C = ( n e. NN |-> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
Assertion	ovnsubadd2lem	|- ( ph -> ( ( voln* ` X ) ` ( A u. B ) ) <_ ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd2lem.x	|- ( ph -> X e. Fin )
2		ovnsubadd2lem.a	|- ( ph -> A C_ ( RR ^m X ) )
3		ovnsubadd2lem.b	|- ( ph -> B C_ ( RR ^m X ) )
4		ovnsubadd2lem.c	|- C = ( n e. NN |-> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
5		iftrue	|- ( n = 1 -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = A )
6	5	adantl	|- ( ( ph /\ n = 1 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = A )
7		ovexd	|- ( ph -> ( RR ^m X ) e. _V )
8	7 2	ssexd	|- ( ph -> A e. _V )
9	8 2	elpwd	|- ( ph -> A e. ~P ( RR ^m X ) )
10	9	adantr	|- ( ( ph /\ n = 1 ) -> A e. ~P ( RR ^m X ) )
11	6 10	eqeltrd	|- ( ( ph /\ n = 1 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
12	11	adantlr	|- ( ( ( ph /\ n e. NN ) /\ n = 1 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
13		simpl	|- ( ( -. n = 1 /\ n = 2 ) -> -. n = 1 )
14	13	iffalsed	|- ( ( -. n = 1 /\ n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = if ( n = 2 , B , (/) ) )
15		simpr	|- ( ( -. n = 1 /\ n = 2 ) -> n = 2 )
16	15	iftrued	|- ( ( -. n = 1 /\ n = 2 ) -> if ( n = 2 , B , (/) ) = B )
17	14 16	eqtrd	|- ( ( -. n = 1 /\ n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = B )
18	17	adantll	|- ( ( ( ph /\ -. n = 1 ) /\ n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = B )
19	7 3	ssexd	|- ( ph -> B e. _V )
20	19 3	elpwd	|- ( ph -> B e. ~P ( RR ^m X ) )
21	20	ad2antrr	|- ( ( ( ph /\ -. n = 1 ) /\ n = 2 ) -> B e. ~P ( RR ^m X ) )
22	18 21	eqeltrd	|- ( ( ( ph /\ -. n = 1 ) /\ n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
23	22	adantllr	|- ( ( ( ( ph /\ n e. NN ) /\ -. n = 1 ) /\ n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
24		simpl	|- ( ( -. n = 1 /\ -. n = 2 ) -> -. n = 1 )
25	24	iffalsed	|- ( ( -. n = 1 /\ -. n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = if ( n = 2 , B , (/) ) )
26		simpr	|- ( ( -. n = 1 /\ -. n = 2 ) -> -. n = 2 )
27	26	iffalsed	|- ( ( -. n = 1 /\ -. n = 2 ) -> if ( n = 2 , B , (/) ) = (/) )
28	25 27	eqtrd	|- ( ( -. n = 1 /\ -. n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = (/) )
29		0elpw	|- (/) e. ~P ( RR ^m X )
30	29	a1i	|- ( ( -. n = 1 /\ -. n = 2 ) -> (/) e. ~P ( RR ^m X ) )
31	28 30	eqeltrd	|- ( ( -. n = 1 /\ -. n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
32	31	adantll	|- ( ( ( ( ph /\ n e. NN ) /\ -. n = 1 ) /\ -. n = 2 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
33	23 32	pm2.61dan	|- ( ( ( ph /\ n e. NN ) /\ -. n = 1 ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
34	12 33	pm2.61dan	|- ( ( ph /\ n e. NN ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. ~P ( RR ^m X ) )
35	34 4	fmptd	|- ( ph -> C : NN --> ~P ( RR ^m X ) )
36	1 35	ovnsubadd	|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( C ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) )
37		eldifi	|- ( n e. ( NN \ { 1 , 2 } ) -> n e. NN )
38	37	adantl	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> n e. NN )
39		eldifn	|- ( n e. ( NN \ { 1 , 2 } ) -> -. n e. { 1 , 2 } )
40		vex	|- n e. _V
41	40	a1i	|- ( -. n e. { 1 , 2 } -> n e. _V )
42		id	|- ( -. n e. { 1 , 2 } -> -. n e. { 1 , 2 } )
43	41 42	nelpr1	|- ( -. n e. { 1 , 2 } -> n =/= 1 )
44	43	neneqd	|- ( -. n e. { 1 , 2 } -> -. n = 1 )
45	39 44	syl	|- ( n e. ( NN \ { 1 , 2 } ) -> -. n = 1 )
46	41 42	nelpr2	|- ( -. n e. { 1 , 2 } -> n =/= 2 )
47	46	neneqd	|- ( -. n e. { 1 , 2 } -> -. n = 2 )
48	39 47	syl	|- ( n e. ( NN \ { 1 , 2 } ) -> -. n = 2 )
49	45 48 28	syl2anc	|- ( n e. ( NN \ { 1 , 2 } ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = (/) )
50		0ex	|- (/) e. _V
51	50	a1i	|- ( n e. ( NN \ { 1 , 2 } ) -> (/) e. _V )
52	49 51	eqeltrd	|- ( n e. ( NN \ { 1 , 2 } ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. _V )
53	52	adantl	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. _V )
54	4	fvmpt2	|- ( ( n e. NN /\ if ( n = 1 , A , if ( n = 2 , B , (/) ) ) e. _V ) -> ( C ` n ) = if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
55	38 53 54	syl2anc	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> ( C ` n ) = if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
56	49	adantl	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = (/) )
57	55 56	eqtrd	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> ( C ` n ) = (/) )
58	57	ralrimiva	|- ( ph -> A. n e. ( NN \ { 1 , 2 } ) ( C ` n ) = (/) )
59		nfcv	|- F/_ n ( NN \ { 1 , 2 } )
60	59	iunxdif3	|- ( A. n e. ( NN \ { 1 , 2 } ) ( C ` n ) = (/) -> U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) = U_ n e. NN ( C ` n ) )
61	58 60	syl	|- ( ph -> U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) = U_ n e. NN ( C ` n ) )
62	61	eqcomd	|- ( ph -> U_ n e. NN ( C ` n ) = U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) )
63		1nn	|- 1 e. NN
64		2nn	|- 2 e. NN
65	63 64	pm3.2i	|- ( 1 e. NN /\ 2 e. NN )
66		prssi	|- ( ( 1 e. NN /\ 2 e. NN ) -> { 1 , 2 } C_ NN )
67	65 66	ax-mp	|- { 1 , 2 } C_ NN
68		dfss4	|- ( { 1 , 2 } C_ NN <-> ( NN \ ( NN \ { 1 , 2 } ) ) = { 1 , 2 } )
69	67 68	mpbi	|- ( NN \ ( NN \ { 1 , 2 } ) ) = { 1 , 2 }
70		iuneq1	|- ( ( NN \ ( NN \ { 1 , 2 } ) ) = { 1 , 2 } -> U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) = U_ n e. { 1 , 2 } ( C ` n ) )
71	69 70	ax-mp	|- U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) = U_ n e. { 1 , 2 } ( C ` n )
72	71	a1i	|- ( ph -> U_ n e. ( NN \ ( NN \ { 1 , 2 } ) ) ( C ` n ) = U_ n e. { 1 , 2 } ( C ` n ) )
73		fveq2	|- ( n = 1 -> ( C ` n ) = ( C ` 1 ) )
74		fveq2	|- ( n = 2 -> ( C ` n ) = ( C ` 2 ) )
75	73 74	iunxprg	|- ( ( 1 e. NN /\ 2 e. NN ) -> U_ n e. { 1 , 2 } ( C ` n ) = ( ( C ` 1 ) u. ( C ` 2 ) ) )
76	63 64 75	mp2an	|- U_ n e. { 1 , 2 } ( C ` n ) = ( ( C ` 1 ) u. ( C ` 2 ) )
77	76	a1i	|- ( ph -> U_ n e. { 1 , 2 } ( C ` n ) = ( ( C ` 1 ) u. ( C ` 2 ) ) )
78	63	a1i	|- ( ph -> 1 e. NN )
79	4 5 78 8	fvmptd3	|- ( ph -> ( C ` 1 ) = A )
80		id	|- ( n = 2 -> n = 2 )
81		1ne2	|- 1 =/= 2
82	81	necomi	|- 2 =/= 1
83	82	a1i	|- ( n = 2 -> 2 =/= 1 )
84	80 83	eqnetrd	|- ( n = 2 -> n =/= 1 )
85	84	neneqd	|- ( n = 2 -> -. n = 1 )
86	85	iffalsed	|- ( n = 2 -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = if ( n = 2 , B , (/) ) )
87		iftrue	|- ( n = 2 -> if ( n = 2 , B , (/) ) = B )
88	86 87	eqtrd	|- ( n = 2 -> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) = B )
89	64	a1i	|- ( ph -> 2 e. NN )
90	4 88 89 19	fvmptd3	|- ( ph -> ( C ` 2 ) = B )
91	79 90	uneq12d	|- ( ph -> ( ( C ` 1 ) u. ( C ` 2 ) ) = ( A u. B ) )
92		eqidd	|- ( ph -> ( A u. B ) = ( A u. B ) )
93	77 91 92	3eqtrd	|- ( ph -> U_ n e. { 1 , 2 } ( C ` n ) = ( A u. B ) )
94	62 72 93	3eqtrd	|- ( ph -> U_ n e. NN ( C ` n ) = ( A u. B ) )
95	94	fveq2d	|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( C ` n ) ) = ( ( voln* ` X ) ` ( A u. B ) ) )
96		nfv	|- F/ n ph
97		nnex	|- NN e. _V
98	97	a1i	|- ( ph -> NN e. _V )
99	67	a1i	|- ( ph -> { 1 , 2 } C_ NN )
100	1	adantr	|- ( ( ph /\ n e. { 1 , 2 } ) -> X e. Fin )
101		simpl	|- ( ( ph /\ n e. { 1 , 2 } ) -> ph )
102	99	sselda	|- ( ( ph /\ n e. { 1 , 2 } ) -> n e. NN )
103	35	ffvelcdmda	|- ( ( ph /\ n e. NN ) -> ( C ` n ) e. ~P ( RR ^m X ) )
104		elpwi	|- ( ( C ` n ) e. ~P ( RR ^m X ) -> ( C ` n ) C_ ( RR ^m X ) )
105	103 104	syl	|- ( ( ph /\ n e. NN ) -> ( C ` n ) C_ ( RR ^m X ) )
106	101 102 105	syl2anc	|- ( ( ph /\ n e. { 1 , 2 } ) -> ( C ` n ) C_ ( RR ^m X ) )
107	100 106	ovncl	|- ( ( ph /\ n e. { 1 , 2 } ) -> ( ( voln* ` X ) ` ( C ` n ) ) e. ( 0 [,] +oo ) )
108	57	fveq2d	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> ( ( voln* ` X ) ` ( C ` n ) ) = ( ( voln* ` X ) ` (/) ) )
109	1	adantr	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> X e. Fin )
110	109	ovn0	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> ( ( voln* ` X ) ` (/) ) = 0 )
111	108 110	eqtrd	|- ( ( ph /\ n e. ( NN \ { 1 , 2 } ) ) -> ( ( voln* ` X ) ` ( C ` n ) ) = 0 )
112	96 98 99 107 111	sge0ss	|- ( ph -> ( sum^ ` ( n e. { 1 , 2 } |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) )
113	112	eqcomd	|- ( ph -> ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) = ( sum^ ` ( n e. { 1 , 2 } |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) )
114	79 2	eqsstrd	|- ( ph -> ( C ` 1 ) C_ ( RR ^m X ) )
115	1 114	ovncl	|- ( ph -> ( ( voln* ` X ) ` ( C ` 1 ) ) e. ( 0 [,] +oo ) )
116	90 3	eqsstrd	|- ( ph -> ( C ` 2 ) C_ ( RR ^m X ) )
117	1 116	ovncl	|- ( ph -> ( ( voln* ` X ) ` ( C ` 2 ) ) e. ( 0 [,] +oo ) )
118		2fveq3	|- ( n = 1 -> ( ( voln* ` X ) ` ( C ` n ) ) = ( ( voln* ` X ) ` ( C ` 1 ) ) )
119		2fveq3	|- ( n = 2 -> ( ( voln* ` X ) ` ( C ` n ) ) = ( ( voln* ` X ) ` ( C ` 2 ) ) )
120	81	a1i	|- ( ph -> 1 =/= 2 )
121	78 89 115 117 118 119 120	sge0pr	|- ( ph -> ( sum^ ` ( n e. { 1 , 2 } |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) = ( ( ( voln* ` X ) ` ( C ` 1 ) ) +e ( ( voln* ` X ) ` ( C ` 2 ) ) ) )
122	79	fveq2d	|- ( ph -> ( ( voln* ` X ) ` ( C ` 1 ) ) = ( ( voln* ` X ) ` A ) )
123	90	fveq2d	|- ( ph -> ( ( voln* ` X ) ` ( C ` 2 ) ) = ( ( voln* ` X ) ` B ) )
124	122 123	oveq12d	|- ( ph -> ( ( ( voln* ` X ) ` ( C ` 1 ) ) +e ( ( voln* ` X ) ` ( C ` 2 ) ) ) = ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )
125	113 121 124	3eqtrd	|- ( ph -> ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) = ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )
126	95 125	breq12d	|- ( ph -> ( ( ( voln* ` X ) ` U_ n e. NN ( C ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( C ` n ) ) ) ) <-> ( ( voln* ` X ) ` ( A u. B ) ) <_ ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) ) )
127	36 126	mpbid	|- ( ph -> ( ( voln* ` X ) ` ( A u. B ) ) <_ ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )