Metamath Proof Explorer


Theorem measvunilem0

Description: Lemma for measvuni . (Contributed by Thierry Arnoux, 6-Mar-2017)

Ref Expression
Hypothesis measvunilem.0.1 _ x A
Assertion measvunilem0 M measures S x A B A ω Disj x A B M x A B = * x A M B

Proof

Step Hyp Ref Expression
1 measvunilem.0.1 _ x A
2 simp3l M measures S x A B A ω Disj x A B A ω
3 ctex A ω A V
4 1 esum0 A V * x A 0 = 0
5 2 3 4 3syl M measures S x A B A ω Disj x A B * x A 0 = 0
6 nfv x M measures S
7 nfra1 x x A B
8 nfcv _ x
9 nfcv _ x ω
10 1 8 9 nfbr x A ω
11 nfdisj1 x Disj x A B
12 10 11 nfan x A ω Disj x A B
13 6 7 12 nf3an x M measures S x A B A ω Disj x A B
14 eqidd M measures S x A B A ω Disj x A B A = A
15 simp2 M measures S x A B A ω Disj x A B x A B
16 15 r19.21bi M measures S x A B A ω Disj x A B x A B
17 elsni B B =
18 16 17 syl M measures S x A B A ω Disj x A B x A B =
19 18 fveq2d M measures S x A B A ω Disj x A B x A M B = M
20 measvnul M measures S M = 0
21 20 3ad2ant1 M measures S x A B A ω Disj x A B M = 0
22 21 adantr M measures S x A B A ω Disj x A B x A M = 0
23 19 22 eqtrd M measures S x A B A ω Disj x A B x A M B = 0
24 13 14 23 esumeq12dvaf M measures S x A B A ω Disj x A B * x A M B = * x A 0
25 13 1 1 14 18 iuneq12daf M measures S x A B A ω Disj x A B x A B = x A
26 iun0 x A =
27 25 26 eqtrdi M measures S x A B A ω Disj x A B x A B =
28 27 fveq2d M measures S x A B A ω Disj x A B M x A B = M
29 28 21 eqtrd M measures S x A B A ω Disj x A B M x A B = 0
30 5 24 29 3eqtr4rd M measures S x A B A ω Disj x A B M x A B = * x A M B