Metamath Proof Explorer

Theorem carsgclctunlem1

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 23-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1 
|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2 
|- ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
fiunelcarsg.1 
|- ( ph -> A e. Fin )
fiunelcarsg.2 
|- ( ph -> A C_ ( toCaraSiga ` M ) )
carsgclctunlem1.1 
|- ( ph -> Disj_ y e. A y )
carsgclctunlem1.2 
|- ( ph -> E e. ~P O )
Assertion carsgclctunlem1 
|- ( ph -> ( M ` ( E i^i U. A ) ) = sum* y e. A ( M ` ( E i^i y ) ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 carsgsiga.1 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 carsgsiga.2 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
5 fiunelcarsg.1 
 |-  ( ph -> A e. Fin )
6 fiunelcarsg.2 
 |-  ( ph -> A C_ ( toCaraSiga ` M ) )
7 carsgclctunlem1.1 
 |-  ( ph -> Disj_ y e. A y )
8 carsgclctunlem1.2 
 |-  ( ph -> E e. ~P O )
9 unieq 
 |-  ( a = (/) -> U. a = U. (/) )
10 9 ineq2d 
 |-  ( a = (/) -> ( E i^i U. a ) = ( E i^i U. (/) ) )
11 10 fveq2d 
 |-  ( a = (/) -> ( M ` ( E i^i U. a ) ) = ( M ` ( E i^i U. (/) ) ) )
12 esumeq1 
 |-  ( a = (/) -> sum* y e. a ( M ` ( E i^i y ) ) = sum* y e. (/) ( M ` ( E i^i y ) ) )
13 11 12 eqeq12d 
 |-  ( a = (/) -> ( ( M ` ( E i^i U. a ) ) = sum* y e. a ( M ` ( E i^i y ) ) <-> ( M ` ( E i^i U. (/) ) ) = sum* y e. (/) ( M ` ( E i^i y ) ) ) )
14 unieq 
 |-  ( a = b -> U. a = U. b )
15 14 ineq2d 
 |-  ( a = b -> ( E i^i U. a ) = ( E i^i U. b ) )
16 15 fveq2d 
 |-  ( a = b -> ( M ` ( E i^i U. a ) ) = ( M ` ( E i^i U. b ) ) )
17 esumeq1 
 |-  ( a = b -> sum* y e. a ( M ` ( E i^i y ) ) = sum* y e. b ( M ` ( E i^i y ) ) )
18 16 17 eqeq12d 
 |-  ( a = b -> ( ( M ` ( E i^i U. a ) ) = sum* y e. a ( M ` ( E i^i y ) ) <-> ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) )
19 unieq 
 |-  ( a = ( b u. { x } ) -> U. a = U. ( b u. { x } ) )
20 19 ineq2d 
 |-  ( a = ( b u. { x } ) -> ( E i^i U. a ) = ( E i^i U. ( b u. { x } ) ) )
21 20 fveq2d 
 |-  ( a = ( b u. { x } ) -> ( M ` ( E i^i U. a ) ) = ( M ` ( E i^i U. ( b u. { x } ) ) ) )
22 esumeq1 
 |-  ( a = ( b u. { x } ) -> sum* y e. a ( M ` ( E i^i y ) ) = sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) )
23 21 22 eqeq12d 
 |-  ( a = ( b u. { x } ) -> ( ( M ` ( E i^i U. a ) ) = sum* y e. a ( M ` ( E i^i y ) ) <-> ( M ` ( E i^i U. ( b u. { x } ) ) ) = sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) ) )
24 unieq 
 |-  ( a = A -> U. a = U. A )
25 24 ineq2d 
 |-  ( a = A -> ( E i^i U. a ) = ( E i^i U. A ) )
26 25 fveq2d 
 |-  ( a = A -> ( M ` ( E i^i U. a ) ) = ( M ` ( E i^i U. A ) ) )
27 esumeq1 
 |-  ( a = A -> sum* y e. a ( M ` ( E i^i y ) ) = sum* y e. A ( M ` ( E i^i y ) ) )
28 26 27 eqeq12d 
 |-  ( a = A -> ( ( M ` ( E i^i U. a ) ) = sum* y e. a ( M ` ( E i^i y ) ) <-> ( M ` ( E i^i U. A ) ) = sum* y e. A ( M ` ( E i^i y ) ) ) )
29 uni0 
 |-  U. (/) = (/)
30 29 ineq2i 
 |-  ( E i^i U. (/) ) = ( E i^i (/) )
31 in0 
 |-  ( E i^i (/) ) = (/)
32 30 31 eqtri 
 |-  ( E i^i U. (/) ) = (/)
33 32 fveq2i 
 |-  ( M ` ( E i^i U. (/) ) ) = ( M ` (/) )
34 esumnul 
 |-  sum* y e. (/) ( M ` ( E i^i y ) ) = 0
35 3 33 34 3eqtr4g 
 |-  ( ph -> ( M ` ( E i^i U. (/) ) ) = sum* y e. (/) ( M ` ( E i^i y ) ) )
36 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) )
37 36 eqcomd 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> sum* y e. b ( M ` ( E i^i y ) ) = ( M ` ( E i^i U. b ) ) )
38 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y = x ) -> y = x )
39 38 ineq2d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y = x ) -> ( E i^i y ) = ( E i^i x ) )
40 39 fveq2d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y = x ) -> ( M ` ( E i^i y ) ) = ( M ` ( E i^i x ) ) )
41 simprr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> x e. ( A \ b ) )
42 2 adantr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> M : ~P O --> ( 0 [,] +oo ) )
43 8 adantr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> E e. ~P O )
44 43 elpwincl1 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i x ) e. ~P O )
45 42 44 ffvelcdmd 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( M ` ( E i^i x ) ) e. ( 0 [,] +oo ) )
46 40 41 45 esumsn 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> sum* y e. { x } ( M ` ( E i^i y ) ) = ( M ` ( E i^i x ) ) )
47 46 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> sum* y e. { x } ( M ` ( E i^i y ) ) = ( M ` ( E i^i x ) ) )
48 37 47 oveq12d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> ( sum* y e. b ( M ` ( E i^i y ) ) +e sum* y e. { x } ( M ` ( E i^i y ) ) ) = ( ( M ` ( E i^i U. b ) ) +e ( M ` ( E i^i x ) ) ) )
49 nfv 
 |-  F/ y ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) )
50 nfcv 
 |-  F/_ y b
51 nfcv 
 |-  F/_ y { x }
52 vex 
 |-  b e. _V
53 52 a1i 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> b e. _V )
54 vsnex 
 |-  { x } e. _V
55 54 a1i 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> { x } e. _V )
56 41 eldifbd 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> -. x e. b )
57 disjsn 
 |-  ( ( b i^i { x } ) = (/) <-> -. x e. b )
58 56 57 sylibr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( b i^i { x } ) = (/) )
59 2 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. b ) -> M : ~P O --> ( 0 [,] +oo ) )
60 8 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. b ) -> E e. ~P O )
61 60 elpwincl1 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. b ) -> ( E i^i y ) e. ~P O )
62 59 61 ffvelcdmd 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. b ) -> ( M ` ( E i^i y ) ) e. ( 0 [,] +oo ) )
63 2 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. { x } ) -> M : ~P O --> ( 0 [,] +oo ) )
64 8 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. { x } ) -> E e. ~P O )
65 64 elpwincl1 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. { x } ) -> ( E i^i y ) e. ~P O )
66 63 65 ffvelcdmd 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ y e. { x } ) -> ( M ` ( E i^i y ) ) e. ( 0 [,] +oo ) )
67 49 50 51 53 55 58 62 66 esumsplit 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) = ( sum* y e. b ( M ` ( E i^i y ) ) +e sum* y e. { x } ( M ` ( E i^i y ) ) ) )
68 67 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) = ( sum* y e. b ( M ` ( E i^i y ) ) +e sum* y e. { x } ( M ` ( E i^i y ) ) ) )
69 uniun 
 |-  U. ( b u. { x } ) = ( U. b u. U. { x } )
70 unisnv 
 |-  U. { x } = x
71 70 uneq2i 
 |-  ( U. b u. U. { x } ) = ( U. b u. x )
72 69 71 eqtri 
 |-  U. ( b u. { x } ) = ( U. b u. x )
73 72 ineq2i 
 |-  ( E i^i U. ( b u. { x } ) ) = ( E i^i ( U. b u. x ) )
74 73 fveq2i 
 |-  ( M ` ( E i^i U. ( b u. { x } ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) )
75 inass 
 |-  ( ( E i^i ( U. b u. x ) ) i^i U. b ) = ( E i^i ( ( U. b u. x ) i^i U. b ) )
76 indir 
 |-  ( ( U. b u. x ) i^i U. b ) = ( ( U. b i^i U. b ) u. ( x i^i U. b ) )
77 inidm 
 |-  ( U. b i^i U. b ) = U. b
78 77 a1i 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( U. b i^i U. b ) = U. b )
79 incom 
 |-  ( U. b i^i x ) = ( x i^i U. b )
80 7 adantr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> Disj_ y e. A y )
81 simpr 
 |-  ( ( ph /\ b C_ A ) -> b C_ A )
82 81 adantrr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> b C_ A )
83 80 82 41 disjuniel 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( U. b i^i x ) = (/) )
84 79 83 eqtr3id 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( x i^i U. b ) = (/) )
85 78 84 uneq12d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b i^i U. b ) u. ( x i^i U. b ) ) = ( U. b u. (/) ) )
86 un0 
 |-  ( U. b u. (/) ) = U. b
87 85 86 eqtrdi 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b i^i U. b ) u. ( x i^i U. b ) ) = U. b )
88 76 87 eqtrid 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b u. x ) i^i U. b ) = U. b )
89 88 ineq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i ( ( U. b u. x ) i^i U. b ) ) = ( E i^i U. b ) )
90 75 89 eqtrid 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( E i^i ( U. b u. x ) ) i^i U. b ) = ( E i^i U. b ) )
91 90 fveq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) = ( M ` ( E i^i U. b ) ) )
92 indif2 
 |-  ( E i^i ( ( U. b u. x ) \ U. b ) ) = ( ( E i^i ( U. b u. x ) ) \ U. b )
93 uncom 
 |-  ( U. b u. x ) = ( x u. U. b )
94 93 difeq1i 
 |-  ( ( U. b u. x ) \ U. b ) = ( ( x u. U. b ) \ U. b )
95 difun2 
 |-  ( ( x u. U. b ) \ U. b ) = ( x \ U. b )
96 disj3 
 |-  ( ( x i^i U. b ) = (/) <-> x = ( x \ U. b ) )
97 96 biimpi 
 |-  ( ( x i^i U. b ) = (/) -> x = ( x \ U. b ) )
98 95 97 eqtr4id 
 |-  ( ( x i^i U. b ) = (/) -> ( ( x u. U. b ) \ U. b ) = x )
99 94 98 eqtrid 
 |-  ( ( x i^i U. b ) = (/) -> ( ( U. b u. x ) \ U. b ) = x )
100 84 99 syl 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b u. x ) \ U. b ) = x )
101 100 ineq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i ( ( U. b u. x ) \ U. b ) ) = ( E i^i x ) )
102 92 101 eqtr3id 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( E i^i ( U. b u. x ) ) \ U. b ) = ( E i^i x ) )
103 102 fveq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) = ( M ` ( E i^i x ) ) )
104 91 103 oveq12d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) +e ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) ) = ( ( M ` ( E i^i U. b ) ) +e ( M ` ( E i^i x ) ) ) )
105 1 adantr 
 |-  ( ( ph /\ b C_ A ) -> O e. V )
106 2 adantr 
 |-  ( ( ph /\ b C_ A ) -> M : ~P O --> ( 0 [,] +oo ) )
107 3 adantr 
 |-  ( ( ph /\ b C_ A ) -> ( M ` (/) ) = 0 )
108 4 3adant1r 
 |-  ( ( ( ph /\ b C_ A ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
109 ssfi 
 |-  ( ( A e. Fin /\ b C_ A ) -> b e. Fin )
110 5 109 sylan 
 |-  ( ( ph /\ b C_ A ) -> b e. Fin )
111 6 adantr 
 |-  ( ( ph /\ b C_ A ) -> A C_ ( toCaraSiga ` M ) )
112 81 111 sstrd 
 |-  ( ( ph /\ b C_ A ) -> b C_ ( toCaraSiga ` M ) )
113 105 106 107 108 110 112 fiunelcarsg 
 |-  ( ( ph /\ b C_ A ) -> U. b e. ( toCaraSiga ` M ) )
114 1 2 elcarsg 
 |-  ( ph -> ( U. b e. ( toCaraSiga ` M ) <-> ( U. b C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) ) ) )
115 114 adantr 
 |-  ( ( ph /\ b C_ A ) -> ( U. b e. ( toCaraSiga ` M ) <-> ( U. b C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) ) ) )
116 113 115 mpbid 
 |-  ( ( ph /\ b C_ A ) -> ( U. b C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) ) )
117 116 simprd 
 |-  ( ( ph /\ b C_ A ) -> A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) )
118 117 adantrr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) )
119 43 elpwincl1 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i ( U. b u. x ) ) e. ~P O )
120 simpr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> e = ( E i^i ( U. b u. x ) ) )
121 120 ineq1d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( e i^i U. b ) = ( ( E i^i ( U. b u. x ) ) i^i U. b ) )
122 121 fveq2d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( M ` ( e i^i U. b ) ) = ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) )
123 120 difeq1d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( e \ U. b ) = ( ( E i^i ( U. b u. x ) ) \ U. b ) )
124 123 fveq2d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( M ` ( e \ U. b ) ) = ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) )
125 122 124 oveq12d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) +e ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) ) )
126 120 fveq2d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( M ` e ) = ( M ` ( E i^i ( U. b u. x ) ) ) )
127 125 126 eqeq12d 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ e = ( E i^i ( U. b u. x ) ) ) -> ( ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) <-> ( ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) +e ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) ) ) )
128 119 127 rspcdv 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) -> ( ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) +e ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) ) ) )
129 118 128 mpd 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( M ` ( ( E i^i ( U. b u. x ) ) i^i U. b ) ) +e ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) ) )
130 104 129 eqtr3d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( M ` ( E i^i U. b ) ) +e ( M ` ( E i^i x ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) ) )
131 130 adantr 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> ( ( M ` ( E i^i U. b ) ) +e ( M ` ( E i^i x ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) ) )
132 74 131 eqtr4id 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> ( M ` ( E i^i U. ( b u. { x } ) ) ) = ( ( M ` ( E i^i U. b ) ) +e ( M ` ( E i^i x ) ) ) )
133 48 68 132 3eqtr4rd 
 |-  ( ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) /\ ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) ) -> ( M ` ( E i^i U. ( b u. { x } ) ) ) = sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) )
134 133 ex 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( M ` ( E i^i U. b ) ) = sum* y e. b ( M ` ( E i^i y ) ) -> ( M ` ( E i^i U. ( b u. { x } ) ) ) = sum* y e. ( b u. { x } ) ( M ` ( E i^i y ) ) ) )
135 13 18 23 28 35 134 5 findcard2d 
 |-  ( ph -> ( M ` ( E i^i U. A ) ) = sum* y e. A ( M ` ( E i^i y ) ) )