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 ffvelrnd 
 |-  ( ( 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 snex 
 |-  { 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 ffvelrnd 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( ( 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 vex 
 |-  x e. _V
71 70 unisn 
 |-  U. { x } = x
72 71 uneq2i 
 |-  ( U. b u. U. { x } ) = ( U. b u. x )
73 69 72 eqtri 
 |-  U. ( b u. { x } ) = ( U. b u. x )
74 73 ineq2i 
 |-  ( E i^i U. ( b u. { x } ) ) = ( E i^i ( U. b u. x ) )
75 74 fveq2i 
 |-  ( M ` ( E i^i U. ( b u. { x } ) ) ) = ( M ` ( E i^i ( U. b u. x ) ) )
76 inass 
 |-  ( ( E i^i ( U. b u. x ) ) i^i U. b ) = ( E i^i ( ( U. b u. x ) i^i U. b ) )
77 indir 
 |-  ( ( U. b u. x ) i^i U. b ) = ( ( U. b i^i U. b ) u. ( x i^i U. b ) )
78 inidm 
 |-  ( U. b i^i U. b ) = U. b
79 78 a1i 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( U. b i^i U. b ) = U. b )
80 incom 
 |-  ( U. b i^i x ) = ( x i^i U. b )
81 7 adantr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> Disj_ y e. A y )
82 simpr 
 |-  ( ( ph /\ b C_ A ) -> b C_ A )
83 82 adantrr 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> b C_ A )
84 81 83 41 disjuniel 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( U. b i^i x ) = (/) )
85 80 84 eqtr3id 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( x i^i U. b ) = (/) )
86 79 85 uneq12d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b i^i U. b ) u. ( x i^i U. b ) ) = ( U. b u. (/) ) )
87 un0 
 |-  ( U. b u. (/) ) = U. b
88 86 87 eqtrdi 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b i^i U. b ) u. ( x i^i U. b ) ) = U. b )
89 77 88 syl5eq 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b u. x ) i^i U. b ) = U. b )
90 89 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 ) )
91 76 90 syl5eq 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( E i^i ( U. b u. x ) ) i^i U. b ) = ( E i^i U. b ) )
92 91 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 ) ) )
93 indif2 
 |-  ( E i^i ( ( U. b u. x ) \ U. b ) ) = ( ( E i^i ( U. b u. x ) ) \ U. b )
94 uncom 
 |-  ( U. b u. x ) = ( x u. U. b )
95 94 difeq1i 
 |-  ( ( U. b u. x ) \ U. b ) = ( ( x u. U. b ) \ U. b )
96 difun2 
 |-  ( ( x u. U. b ) \ U. b ) = ( x \ U. b )
97 disj3 
 |-  ( ( x i^i U. b ) = (/) <-> x = ( x \ U. b ) )
98 97 biimpi 
 |-  ( ( x i^i U. b ) = (/) -> x = ( x \ U. b ) )
99 96 98 eqtr4id 
 |-  ( ( x i^i U. b ) = (/) -> ( ( x u. U. b ) \ U. b ) = x )
100 95 99 syl5eq 
 |-  ( ( x i^i U. b ) = (/) -> ( ( U. b u. x ) \ U. b ) = x )
101 85 100 syl 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( U. b u. x ) \ U. b ) = x )
102 101 ineq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i ( ( U. b u. x ) \ U. b ) ) = ( E i^i x ) )
103 93 102 eqtr3id 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( ( E i^i ( U. b u. x ) ) \ U. b ) = ( E i^i x ) )
104 103 fveq2d 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( M ` ( ( E i^i ( U. b u. x ) ) \ U. b ) ) = ( M ` ( E i^i x ) ) )
105 92 104 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 ) ) ) )
106 1 adantr 
 |-  ( ( ph /\ b C_ A ) -> O e. V )
107 2 adantr 
 |-  ( ( ph /\ b C_ A ) -> M : ~P O --> ( 0 [,] +oo ) )
108 3 adantr 
 |-  ( ( ph /\ b C_ A ) -> ( M ` (/) ) = 0 )
109 4 3adant1r 
 |-  ( ( ( ph /\ b C_ A ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
110 ssfi 
 |-  ( ( A e. Fin /\ b C_ A ) -> b e. Fin )
111 5 110 sylan 
 |-  ( ( ph /\ b C_ A ) -> b e. Fin )
112 6 adantr 
 |-  ( ( ph /\ b C_ A ) -> A C_ ( toCaraSiga ` M ) )
113 82 112 sstrd 
 |-  ( ( ph /\ b C_ A ) -> b C_ ( toCaraSiga ` M ) )
114 106 107 108 109 111 113 fiunelcarsg 
 |-  ( ( ph /\ b C_ A ) -> U. b e. ( toCaraSiga ` M ) )
115 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 ) ) ) )
116 115 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 ) ) ) )
117 114 116 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 ) ) )
118 117 simprd 
 |-  ( ( ph /\ b C_ A ) -> A. e e. ~P O ( ( M ` ( e i^i U. b ) ) +e ( M ` ( e \ U. b ) ) ) = ( M ` e ) )
119 118 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 ) )
120 43 elpwincl1 
 |-  ( ( ph /\ ( b C_ A /\ x e. ( A \ b ) ) ) -> ( E i^i ( U. b u. x ) ) e. ~P O )
121 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 ) ) )
122 121 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 ) )
123 122 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 ) ) )
124 121 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 ) )
125 124 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 ) ) )
126 123 125 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 ) ) ) )
127 121 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 ) ) ) )
128 126 127 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 ) ) ) ) )
129 120 128 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 ) ) ) ) )
130 119 129 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 ) ) ) )
131 105 130 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 ) ) ) )
132 131 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 ) ) ) )
133 75 132 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 ) ) ) )
134 48 68 133 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 ) ) )
135 134 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 ) ) ) )
136 13 18 23 28 35 135 5 findcard2d 
 |-  ( ph -> ( M ` ( E i^i U. A ) ) = sum* y e. A ( M ` ( E i^i y ) ) )