Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carsgclctunlem1 Structured version   Visualization version   GIF version

Theorem carsgclctunlem1 30849
Description: Lemma for carsgclctun 30853. (Contributed by Thierry Arnoux, 23-May-2020.)
Hypotheses
Ref Expression
carsgval.1 (𝜑𝑂𝑉)
carsgval.2 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
carsgsiga.1 (𝜑 → (𝑀‘∅) = 0)
carsgsiga.2 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
fiunelcarsg.1 (𝜑𝐴 ∈ Fin)
fiunelcarsg.2 (𝜑𝐴 ⊆ (toCaraSiga‘𝑀))
carsgclctunlem1.1 (𝜑Disj 𝑦𝐴 𝑦)
carsgclctunlem1.2 (𝜑𝐸 ∈ 𝒫 𝑂)
Assertion
Ref Expression
carsgclctunlem1 (𝜑 → (𝑀‘(𝐸 𝐴)) = Σ*𝑦𝐴(𝑀‘(𝐸𝑦)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐸,𝑦   𝑥,𝑀,𝑦   𝑥,𝑂,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem carsgclctunlem1
Dummy variables 𝑎 𝑒 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4604 . . . . 5 (𝑎 = ∅ → 𝑎 = ∅)
21ineq2d 3978 . . . 4 (𝑎 = ∅ → (𝐸 𝑎) = (𝐸 ∅))
32fveq2d 6383 . . 3 (𝑎 = ∅ → (𝑀‘(𝐸 𝑎)) = (𝑀‘(𝐸 ∅)))
4 esumeq1 30566 . . 3 (𝑎 = ∅ → Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸𝑦)))
53, 4eqeq12d 2780 . 2 (𝑎 = ∅ → ((𝑀‘(𝐸 𝑎)) = Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) ↔ (𝑀‘(𝐸 ∅)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸𝑦))))
6 unieq 4604 . . . . 5 (𝑎 = 𝑏 𝑎 = 𝑏)
76ineq2d 3978 . . . 4 (𝑎 = 𝑏 → (𝐸 𝑎) = (𝐸 𝑏))
87fveq2d 6383 . . 3 (𝑎 = 𝑏 → (𝑀‘(𝐸 𝑎)) = (𝑀‘(𝐸 𝑏)))
9 esumeq1 30566 . . 3 (𝑎 = 𝑏 → Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦)))
108, 9eqeq12d 2780 . 2 (𝑎 = 𝑏 → ((𝑀‘(𝐸 𝑎)) = Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) ↔ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))))
11 unieq 4604 . . . . 5 (𝑎 = (𝑏 ∪ {𝑥}) → 𝑎 = (𝑏 ∪ {𝑥}))
1211ineq2d 3978 . . . 4 (𝑎 = (𝑏 ∪ {𝑥}) → (𝐸 𝑎) = (𝐸 (𝑏 ∪ {𝑥})))
1312fveq2d 6383 . . 3 (𝑎 = (𝑏 ∪ {𝑥}) → (𝑀‘(𝐸 𝑎)) = (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))))
14 esumeq1 30566 . . 3 (𝑎 = (𝑏 ∪ {𝑥}) → Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦)))
1513, 14eqeq12d 2780 . 2 (𝑎 = (𝑏 ∪ {𝑥}) → ((𝑀‘(𝐸 𝑎)) = Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) ↔ (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦))))
16 unieq 4604 . . . . 5 (𝑎 = 𝐴 𝑎 = 𝐴)
1716ineq2d 3978 . . . 4 (𝑎 = 𝐴 → (𝐸 𝑎) = (𝐸 𝐴))
1817fveq2d 6383 . . 3 (𝑎 = 𝐴 → (𝑀‘(𝐸 𝑎)) = (𝑀‘(𝐸 𝐴)))
19 esumeq1 30566 . . 3 (𝑎 = 𝐴 → Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) = Σ*𝑦𝐴(𝑀‘(𝐸𝑦)))
2018, 19eqeq12d 2780 . 2 (𝑎 = 𝐴 → ((𝑀‘(𝐸 𝑎)) = Σ*𝑦𝑎(𝑀‘(𝐸𝑦)) ↔ (𝑀‘(𝐸 𝐴)) = Σ*𝑦𝐴(𝑀‘(𝐸𝑦))))
21 carsgsiga.1 . . 3 (𝜑 → (𝑀‘∅) = 0)
22 uni0 4625 . . . . . 6 ∅ = ∅
2322ineq2i 3975 . . . . 5 (𝐸 ∅) = (𝐸 ∩ ∅)
24 in0 4132 . . . . 5 (𝐸 ∩ ∅) = ∅
2523, 24eqtri 2787 . . . 4 (𝐸 ∅) = ∅
2625fveq2i 6382 . . 3 (𝑀‘(𝐸 ∅)) = (𝑀‘∅)
27 esumnul 30580 . . 3 Σ*𝑦 ∈ ∅(𝑀‘(𝐸𝑦)) = 0
2821, 26, 273eqtr4g 2824 . 2 (𝜑 → (𝑀‘(𝐸 ∅)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸𝑦)))
29 simpr 477 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦)))
3029eqcomd 2771 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → Σ*𝑦𝑏(𝑀‘(𝐸𝑦)) = (𝑀‘(𝐸 𝑏)))
31 simpr 477 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
3231ineq2d 3978 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 = 𝑥) → (𝐸𝑦) = (𝐸𝑥))
3332fveq2d 6383 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 = 𝑥) → (𝑀‘(𝐸𝑦)) = (𝑀‘(𝐸𝑥)))
34 simprr 789 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → 𝑥 ∈ (𝐴𝑏))
35 carsgval.2 . . . . . . . . 9 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
3635adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
37 carsgclctunlem1.2 . . . . . . . . . 10 (𝜑𝐸 ∈ 𝒫 𝑂)
3837adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → 𝐸 ∈ 𝒫 𝑂)
3938elpwincl1 29829 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝐸𝑥) ∈ 𝒫 𝑂)
4036, 39ffvelrnd 6554 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝑀‘(𝐸𝑥)) ∈ (0[,]+∞))
4133, 34, 40esumsn 30597 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸𝑦)) = (𝑀‘(𝐸𝑥)))
4241adantr 472 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸𝑦)) = (𝑀‘(𝐸𝑥)))
4330, 42oveq12d 6864 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → (Σ*𝑦𝑏(𝑀‘(𝐸𝑦)) +𝑒 Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸𝑦))) = ((𝑀‘(𝐸 𝑏)) +𝑒 (𝑀‘(𝐸𝑥))))
44 nfv 2009 . . . . . 6 𝑦(𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏)))
45 nfcv 2907 . . . . . 6 𝑦𝑏
46 nfcv 2907 . . . . . 6 𝑦{𝑥}
47 vex 3353 . . . . . . 7 𝑏 ∈ V
4847a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → 𝑏 ∈ V)
49 snex 5066 . . . . . . 7 {𝑥} ∈ V
5049a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → {𝑥} ∈ V)
5134eldifbd 3747 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ¬ 𝑥𝑏)
52 disjsn 4404 . . . . . . 7 ((𝑏 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥𝑏)
5351, 52sylibr 225 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝑏 ∩ {𝑥}) = ∅)
5435ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦𝑏) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
5537ad2antrr 717 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦𝑏) → 𝐸 ∈ 𝒫 𝑂)
5655elpwincl1 29829 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦𝑏) → (𝐸𝑦) ∈ 𝒫 𝑂)
5754, 56ffvelrnd 6554 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦𝑏) → (𝑀‘(𝐸𝑦)) ∈ (0[,]+∞))
5835ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
5937ad2antrr 717 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝐸 ∈ 𝒫 𝑂)
6059elpwincl1 29829 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝐸𝑦) ∈ 𝒫 𝑂)
6158, 60ffvelrnd 6554 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝑀‘(𝐸𝑦)) ∈ (0[,]+∞))
6244, 45, 46, 48, 50, 53, 57, 61esumsplit 30585 . . . . 5 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦)) = (Σ*𝑦𝑏(𝑀‘(𝐸𝑦)) +𝑒 Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸𝑦))))
6362adantr 472 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦)) = (Σ*𝑦𝑏(𝑀‘(𝐸𝑦)) +𝑒 Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸𝑦))))
64 inass 3985 . . . . . . . . . 10 ((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏) = (𝐸 ∩ (( 𝑏𝑥) ∩ 𝑏))
65 indir 4042 . . . . . . . . . . . 12 (( 𝑏𝑥) ∩ 𝑏) = (( 𝑏 𝑏) ∪ (𝑥 𝑏))
66 inidm 3984 . . . . . . . . . . . . . . 15 ( 𝑏 𝑏) = 𝑏
6766a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ( 𝑏 𝑏) = 𝑏)
68 incom 3969 . . . . . . . . . . . . . . 15 ( 𝑏𝑥) = (𝑥 𝑏)
69 carsgclctunlem1.1 . . . . . . . . . . . . . . . . 17 (𝜑Disj 𝑦𝐴 𝑦)
7069adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → Disj 𝑦𝐴 𝑦)
71 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐴) → 𝑏𝐴)
7271adantrr 708 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → 𝑏𝐴)
7370, 72, 34disjuniel 29881 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ( 𝑏𝑥) = ∅)
7468, 73syl5eqr 2813 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝑥 𝑏) = ∅)
7567, 74uneq12d 3932 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (( 𝑏 𝑏) ∪ (𝑥 𝑏)) = ( 𝑏 ∪ ∅))
76 un0 4131 . . . . . . . . . . . . 13 ( 𝑏 ∪ ∅) = 𝑏
7775, 76syl6eq 2815 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (( 𝑏 𝑏) ∪ (𝑥 𝑏)) = 𝑏)
7865, 77syl5eq 2811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (( 𝑏𝑥) ∩ 𝑏) = 𝑏)
7978ineq2d 3978 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝐸 ∩ (( 𝑏𝑥) ∩ 𝑏)) = (𝐸 𝑏))
8064, 79syl5eq 2811 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏) = (𝐸 𝑏))
8180fveq2d 6383 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) = (𝑀‘(𝐸 𝑏)))
82 indif2 4037 . . . . . . . . . 10 (𝐸 ∩ (( 𝑏𝑥) ∖ 𝑏)) = ((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏)
83 uncom 3921 . . . . . . . . . . . . . 14 ( 𝑏𝑥) = (𝑥 𝑏)
8483difeq1i 3888 . . . . . . . . . . . . 13 (( 𝑏𝑥) ∖ 𝑏) = ((𝑥 𝑏) ∖ 𝑏)
85 disj3 4184 . . . . . . . . . . . . . . 15 ((𝑥 𝑏) = ∅ ↔ 𝑥 = (𝑥 𝑏))
8685biimpi 207 . . . . . . . . . . . . . 14 ((𝑥 𝑏) = ∅ → 𝑥 = (𝑥 𝑏))
87 difun2 4210 . . . . . . . . . . . . . 14 ((𝑥 𝑏) ∖ 𝑏) = (𝑥 𝑏)
8886, 87syl6reqr 2818 . . . . . . . . . . . . 13 ((𝑥 𝑏) = ∅ → ((𝑥 𝑏) ∖ 𝑏) = 𝑥)
8984, 88syl5eq 2811 . . . . . . . . . . . 12 ((𝑥 𝑏) = ∅ → (( 𝑏𝑥) ∖ 𝑏) = 𝑥)
9074, 89syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (( 𝑏𝑥) ∖ 𝑏) = 𝑥)
9190ineq2d 3978 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝐸 ∩ (( 𝑏𝑥) ∖ 𝑏)) = (𝐸𝑥))
9282, 91syl5eqr 2813 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏) = (𝐸𝑥))
9392fveq2d 6383 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏)) = (𝑀‘(𝐸𝑥)))
9481, 93oveq12d 6864 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))) = ((𝑀‘(𝐸 𝑏)) +𝑒 (𝑀‘(𝐸𝑥))))
95 carsgval.1 . . . . . . . . . . . . 13 (𝜑𝑂𝑉)
9695adantr 472 . . . . . . . . . . . 12 ((𝜑𝑏𝐴) → 𝑂𝑉)
9735adantr 472 . . . . . . . . . . . 12 ((𝜑𝑏𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
9821adantr 472 . . . . . . . . . . . 12 ((𝜑𝑏𝐴) → (𝑀‘∅) = 0)
99 carsgsiga.2 . . . . . . . . . . . . 13 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
100993adant1r 1223 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
101 fiunelcarsg.1 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ Fin)
102 ssfi 8391 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑏𝐴) → 𝑏 ∈ Fin)
103101, 102sylan 575 . . . . . . . . . . . 12 ((𝜑𝑏𝐴) → 𝑏 ∈ Fin)
104 fiunelcarsg.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ (toCaraSiga‘𝑀))
105104adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑏𝐴) → 𝐴 ⊆ (toCaraSiga‘𝑀))
10671, 105sstrd 3773 . . . . . . . . . . . 12 ((𝜑𝑏𝐴) → 𝑏 ⊆ (toCaraSiga‘𝑀))
10796, 97, 98, 100, 103, 106fiunelcarsg 30848 . . . . . . . . . . 11 ((𝜑𝑏𝐴) → 𝑏 ∈ (toCaraSiga‘𝑀))
10895, 35elcarsg 30837 . . . . . . . . . . . 12 (𝜑 → ( 𝑏 ∈ (toCaraSiga‘𝑀) ↔ ( 𝑏𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒))))
109108adantr 472 . . . . . . . . . . 11 ((𝜑𝑏𝐴) → ( 𝑏 ∈ (toCaraSiga‘𝑀) ↔ ( 𝑏𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒))))
110107, 109mpbid 223 . . . . . . . . . 10 ((𝜑𝑏𝐴) → ( 𝑏𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒)))
111110simprd 489 . . . . . . . . 9 ((𝜑𝑏𝐴) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒))
112111adantrr 708 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒))
11338elpwincl1 29829 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (𝐸 ∩ ( 𝑏𝑥)) ∈ 𝒫 𝑂)
114 simpr 477 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → 𝑒 = (𝐸 ∩ ( 𝑏𝑥)))
115114ineq1d 3977 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (𝑒 𝑏) = ((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏))
116115fveq2d 6383 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (𝑀‘(𝑒 𝑏)) = (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)))
117114difeq1d 3891 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (𝑒 𝑏) = ((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))
118117fveq2d 6383 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (𝑀‘(𝑒 𝑏)) = (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏)))
119116, 118oveq12d 6864 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → ((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = ((𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))))
120114fveq2d 6383 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (𝑀𝑒) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥))))
121119, 120eqeq12d 2780 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ 𝑒 = (𝐸 ∩ ( 𝑏𝑥))) → (((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒) ↔ ((𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥)))))
122113, 121rspcdv 3465 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑏)) +𝑒 (𝑀‘(𝑒 𝑏))) = (𝑀𝑒) → ((𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥)))))
123112, 122mpd 15 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∩ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ ( 𝑏𝑥)) ∖ 𝑏))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥))))
12494, 123eqtr3d 2801 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝑀‘(𝐸 𝑏)) +𝑒 (𝑀‘(𝐸𝑥))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥))))
125124adantr 472 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → ((𝑀‘(𝐸 𝑏)) +𝑒 (𝑀‘(𝐸𝑥))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥))))
126 uniun 4617 . . . . . . . 8 (𝑏 ∪ {𝑥}) = ( 𝑏 {𝑥})
127 vex 3353 . . . . . . . . . 10 𝑥 ∈ V
128127unisn 4612 . . . . . . . . 9 {𝑥} = 𝑥
129128uneq2i 3928 . . . . . . . 8 ( 𝑏 {𝑥}) = ( 𝑏𝑥)
130126, 129eqtri 2787 . . . . . . 7 (𝑏 ∪ {𝑥}) = ( 𝑏𝑥)
131130ineq2i 3975 . . . . . 6 (𝐸 (𝑏 ∪ {𝑥})) = (𝐸 ∩ ( 𝑏𝑥))
132131fveq2i 6382 . . . . 5 (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))) = (𝑀‘(𝐸 ∩ ( 𝑏𝑥)))
133125, 132syl6reqr 2818 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))) = ((𝑀‘(𝐸 𝑏)) +𝑒 (𝑀‘(𝐸𝑥))))
13443, 63, 1333eqtr4rd 2810 . . 3 (((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) ∧ (𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦))) → (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦)))
135134ex 401 . 2 ((𝜑 ∧ (𝑏𝐴𝑥 ∈ (𝐴𝑏))) → ((𝑀‘(𝐸 𝑏)) = Σ*𝑦𝑏(𝑀‘(𝐸𝑦)) → (𝑀‘(𝐸 (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸𝑦))))
1365, 10, 15, 20, 28, 135, 101findcard2d 8413 1 (𝜑 → (𝑀‘(𝐸 𝐴)) = Σ*𝑦𝐴(𝑀‘(𝐸𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336   cuni 4596  Disj wdisj 4779   class class class wbr 4811  wf 6066  cfv 6070  (class class class)co 6846  ωcom 7267  cdom 8162  Fincfn 8164  0cc0 10193  +∞cpnf 10329  cle 10333   +𝑒 cxad 12151  [,]cicc 12387  Σ*cesum 30559  toCaraSigaccarsg 30833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-disj 4780  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-fi 8528  df-sup 8559  df-inf 8560  df-oi 8626  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-div 10944  df-nn 11280  df-2 11340  df-3 11341  df-4 11342  df-5 11343  df-6 11344  df-7 11345  df-8 11346  df-9 11347  df-n0 11544  df-z 11630  df-dec 11747  df-uz 11894  df-q 11997  df-rp 12036  df-xneg 12153  df-xadd 12154  df-xmul 12155  df-ioo 12388  df-ioc 12389  df-ico 12390  df-icc 12391  df-fz 12541  df-fzo 12681  df-fl 12808  df-mod 12884  df-seq 13016  df-exp 13075  df-fac 13272  df-bc 13301  df-hash 13329  df-shft 14108  df-cj 14140  df-re 14141  df-im 14142  df-sqrt 14276  df-abs 14277  df-limsup 14503  df-clim 14520  df-rlim 14521  df-sum 14718  df-ef 15096  df-sin 15098  df-cos 15099  df-pi 15101  df-struct 16148  df-ndx 16149  df-slot 16150  df-base 16152  df-sets 16153  df-ress 16154  df-plusg 16243  df-mulr 16244  df-starv 16245  df-sca 16246  df-vsca 16247  df-ip 16248  df-tset 16249  df-ple 16250  df-ds 16252  df-unif 16253  df-hom 16254  df-cco 16255  df-rest 16365  df-topn 16366  df-0g 16384  df-gsum 16385  df-topgen 16386  df-pt 16387  df-prds 16390  df-ordt 16443  df-xrs 16444  df-qtop 16449  df-imas 16450  df-xps 16452  df-mre 16528  df-mrc 16529  df-acs 16531  df-ps 17482  df-tsr 17483  df-plusf 17523  df-mgm 17524  df-sgrp 17566  df-mnd 17577  df-mhm 17617  df-submnd 17618  df-grp 17708  df-minusg 17709  df-sbg 17710  df-mulg 17824  df-subg 17871  df-cntz 18029  df-cmn 18477  df-abl 18478  df-mgp 18773  df-ur 18785  df-ring 18832  df-cring 18833  df-subrg 19063  df-abv 19102  df-lmod 19150  df-scaf 19151  df-sra 19462  df-rgmod 19463  df-psmet 20027  df-xmet 20028  df-met 20029  df-bl 20030  df-mopn 20031  df-fbas 20032  df-fg 20033  df-cnfld 20036  df-top 20994  df-topon 21011  df-topsp 21033  df-bases 21046  df-cld 21119  df-ntr 21120  df-cls 21121  df-nei 21198  df-lp 21236  df-perf 21237  df-cn 21327  df-cnp 21328  df-haus 21415  df-tx 21661  df-hmeo 21854  df-fil 21945  df-fm 22037  df-flim 22038  df-flf 22039  df-tmd 22171  df-tgp 22172  df-tsms 22225  df-trg 22258  df-xms 22420  df-ms 22421  df-tms 22422  df-nm 22682  df-ngp 22683  df-nrg 22685  df-nlm 22686  df-ii 22975  df-cncf 22976  df-limc 23937  df-dv 23938  df-log 24610  df-esum 30560  df-carsg 30834
This theorem is referenced by:  carsggect  30850  carsgclctunlem2  30851
  Copyright terms: Public domain W3C validator