MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumpropd2lem Structured version   Visualization version   GIF version

Theorem gsumpropd2lem 17735
Description: Lemma for gsumpropd2 17736. (Contributed by Thierry Arnoux, 28-Jun-2017.)
Hypotheses
Ref Expression
gsumpropd2.f (𝜑𝐹𝑉)
gsumpropd2.g (𝜑𝐺𝑊)
gsumpropd2.h (𝜑𝐻𝑋)
gsumpropd2.b (𝜑 → (Base‘𝐺) = (Base‘𝐻))
gsumpropd2.c ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) ∈ (Base‘𝐺))
gsumpropd2.e ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) = (𝑠(+g𝐻)𝑡))
gsumpropd2.n (𝜑 → Fun 𝐹)
gsumpropd2.r (𝜑 → ran 𝐹 ⊆ (Base‘𝐺))
gsumprop2dlem.1 𝐴 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}))
gsumprop2dlem.2 𝐵 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}))
Assertion
Ref Expression
gsumpropd2lem (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Distinct variable groups:   𝑡,𝑠,𝐹   𝐺,𝑠,𝑡   𝐻,𝑠,𝑡   𝜑,𝑠,𝑡
Allowed substitution hints:   𝐴(𝑡,𝑠)   𝐵(𝑡,𝑠)   𝑉(𝑡,𝑠)   𝑊(𝑡,𝑠)   𝑋(𝑡,𝑠)

Proof of Theorem gsumpropd2lem
Dummy variables 𝑎 𝑏 𝑓 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumpropd2.b . . . . 5 (𝜑 → (Base‘𝐺) = (Base‘𝐻))
21adantr 473 . . . . . 6 ((𝜑𝑠 ∈ (Base‘𝐺)) → (Base‘𝐺) = (Base‘𝐻))
3 gsumpropd2.e . . . . . . . . 9 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) = (𝑠(+g𝐻)𝑡))
43eqeq1d 2774 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → ((𝑠(+g𝐺)𝑡) = 𝑡 ↔ (𝑠(+g𝐻)𝑡) = 𝑡))
53oveqrspc2v 6997 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g𝐺)𝑏) = (𝑎(+g𝐻)𝑏))
65oveqrspc2v 6997 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺))) → (𝑡(+g𝐺)𝑠) = (𝑡(+g𝐻)𝑠))
76ancom2s 637 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑡(+g𝐺)𝑠) = (𝑡(+g𝐻)𝑠))
87eqeq1d 2774 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → ((𝑡(+g𝐺)𝑠) = 𝑡 ↔ (𝑡(+g𝐻)𝑠) = 𝑡))
94, 8anbi12d 621 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡) ↔ ((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)))
109anassrs 460 . . . . . 6 (((𝜑𝑠 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ (Base‘𝐺)) → (((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡) ↔ ((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)))
112, 10raleqbidva 3359 . . . . 5 ((𝜑𝑠 ∈ (Base‘𝐺)) → (∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡) ↔ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)))
121, 11rabeqbidva 3403 . . . 4 (𝜑 → {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)})
1312sseq2d 3883 . . 3 (𝜑 → (ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)} ↔ ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}))
14 eqidd 2773 . . . 4 (𝜑 → (Base‘𝐺) = (Base‘𝐺))
1514, 1, 3grpidpropd 17723 . . 3 (𝜑 → (0g𝐺) = (0g𝐻))
16 simprl 758 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) → 𝑛 ∈ (ℤ𝑚))
17 gsumpropd2.r . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 ⊆ (Base‘𝐺))
1817ad2antrr 713 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → ran 𝐹 ⊆ (Base‘𝐺))
19 gsumpropd2.n . . . . . . . . . . . . . 14 (𝜑 → Fun 𝐹)
2019ad2antrr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → Fun 𝐹)
21 simpr 477 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → 𝑠 ∈ (𝑚...𝑛))
22 simplrr 765 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → dom 𝐹 = (𝑚...𝑛))
2321, 22eleqtrrd 2863 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → 𝑠 ∈ dom 𝐹)
24 fvelrn 6663 . . . . . . . . . . . . 13 ((Fun 𝐹𝑠 ∈ dom 𝐹) → (𝐹𝑠) ∈ ran 𝐹)
2520, 23, 24syl2anc 576 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → (𝐹𝑠) ∈ ran 𝐹)
2618, 25sseldd 3853 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ 𝑠 ∈ (𝑚...𝑛)) → (𝐹𝑠) ∈ (Base‘𝐺))
27 gsumpropd2.c . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) ∈ (Base‘𝐺))
2827adantlr 702 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) ∈ (Base‘𝐺))
293adantlr 702 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g𝐺)𝑡) = (𝑠(+g𝐻)𝑡))
3016, 26, 28, 29seqfeq4 13228 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) → (seq𝑚((+g𝐺), 𝐹)‘𝑛) = (seq𝑚((+g𝐻), 𝐹)‘𝑛))
3130eqeq2d 2782 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ𝑚) ∧ dom 𝐹 = (𝑚...𝑛))) → (𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛)))
3231anassrs 460 . . . . . . . 8 (((𝜑𝑛 ∈ (ℤ𝑚)) ∧ dom 𝐹 = (𝑚...𝑛)) → (𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛)))
3332pm5.32da 571 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑚)) → ((dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛)) ↔ (dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))))
3433rexbidva 3235 . . . . . 6 (𝜑 → (∃𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))))
3534exbidv 1880 . . . . 5 (𝜑 → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))))
3635iotabidv 6167 . . . 4 (𝜑 → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))))
3712difeq2d 3983 . . . . . . . . . . . . . . 15 (𝜑 → (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}) = (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}))
3837imaeq2d 5764 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})) = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)})))
39 gsumprop2dlem.1 . . . . . . . . . . . . . 14 𝐴 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}))
40 gsumprop2dlem.2 . . . . . . . . . . . . . 14 𝐵 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}))
4138, 39, 403eqtr4g 2833 . . . . . . . . . . . . 13 (𝜑𝐴 = 𝐵)
4241fveq2d 6497 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) = (♯‘𝐵))
4342fveq2d 6497 . . . . . . . . . . 11 (𝜑 → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)) = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)))
4443adantr 473 . . . . . . . . . 10 ((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)) = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)))
45 simpr 477 . . . . . . . . . . . 12 (((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) → (♯‘𝐵) ∈ (ℤ‘1))
4617ad3antrrr 717 . . . . . . . . . . . . 13 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → ran 𝐹 ⊆ (Base‘𝐺))
47 f1ofun 6440 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → Fun 𝑓)
4847ad3antlr 718 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → Fun 𝑓)
49 simpr 477 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵)))
50 f1odm 6442 . . . . . . . . . . . . . . . . . 18 (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → dom 𝑓 = (1...(♯‘𝐴)))
5150ad3antlr 718 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → dom 𝑓 = (1...(♯‘𝐴)))
5242oveq2d 6986 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...(♯‘𝐴)) = (1...(♯‘𝐵)))
5352ad3antrrr 717 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → (1...(♯‘𝐴)) = (1...(♯‘𝐵)))
5451, 53eqtrd 2808 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → dom 𝑓 = (1...(♯‘𝐵)))
5549, 54eleqtrrd 2863 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → 𝑎 ∈ dom 𝑓)
56 fvco 6581 . . . . . . . . . . . . . . 15 ((Fun 𝑓𝑎 ∈ dom 𝑓) → ((𝐹𝑓)‘𝑎) = (𝐹‘(𝑓𝑎)))
5748, 55, 56syl2anc 576 . . . . . . . . . . . . . 14 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → ((𝐹𝑓)‘𝑎) = (𝐹‘(𝑓𝑎)))
5819ad3antrrr 717 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → Fun 𝐹)
59 difpreima 6654 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝐹 → (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})) = ((𝐹 “ V) ∖ (𝐹 “ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})))
6019, 59syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})) = ((𝐹 “ V) ∖ (𝐹 “ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})))
6139, 60syl5eq 2820 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 = ((𝐹 “ V) ∖ (𝐹 “ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})))
62 difss 3992 . . . . . . . . . . . . . . . . . . 19 ((𝐹 “ V) ∖ (𝐹 “ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})) ⊆ (𝐹 “ V)
6361, 62syl6eqss 3905 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ (𝐹 “ V))
64 dfdm4 5608 . . . . . . . . . . . . . . . . . . 19 dom 𝐹 = ran 𝐹
65 dfrn4 5892 . . . . . . . . . . . . . . . . . . 19 ran 𝐹 = (𝐹 “ V)
6664, 65eqtri 2796 . . . . . . . . . . . . . . . . . 18 dom 𝐹 = (𝐹 “ V)
6763, 66syl6sseqr 3902 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ dom 𝐹)
6867ad3antrrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → 𝐴 ⊆ dom 𝐹)
69 f1of 6438 . . . . . . . . . . . . . . . . . 18 (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑓:(1...(♯‘𝐴))⟶𝐴)
7069ad3antlr 718 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
7149, 53eleqtrrd 2863 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐴)))
7270, 71ffvelrnd 6671 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → (𝑓𝑎) ∈ 𝐴)
7368, 72sseldd 3853 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → (𝑓𝑎) ∈ dom 𝐹)
74 fvelrn 6663 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ (𝑓𝑎) ∈ dom 𝐹) → (𝐹‘(𝑓𝑎)) ∈ ran 𝐹)
7558, 73, 74syl2anc 576 . . . . . . . . . . . . . 14 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → (𝐹‘(𝑓𝑎)) ∈ ran 𝐹)
7657, 75eqeltrd 2860 . . . . . . . . . . . . 13 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → ((𝐹𝑓)‘𝑎) ∈ ran 𝐹)
7746, 76sseldd 3853 . . . . . . . . . . . 12 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ 𝑎 ∈ (1...(♯‘𝐵))) → ((𝐹𝑓)‘𝑎) ∈ (Base‘𝐺))
7827caovclg 7150 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g𝐺)𝑏) ∈ (Base‘𝐺))
7978ad4ant14 739 . . . . . . . . . . . 12 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g𝐺)𝑏) ∈ (Base‘𝐺))
805ad4ant14 739 . . . . . . . . . . . 12 ((((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺))) → (𝑎(+g𝐺)𝑏) = (𝑎(+g𝐻)𝑏))
8145, 77, 79, 80seqfeq4 13228 . . . . . . . . . . 11 (((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ (♯‘𝐵) ∈ (ℤ‘1)) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))
82 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → ¬ (♯‘𝐵) ∈ (ℤ‘1))
83 1z 11819 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
84 seqfn 13190 . . . . . . . . . . . . . . . . 17 (1 ∈ ℤ → seq1((+g𝐺), (𝐹𝑓)) Fn (ℤ‘1))
85 fndm 6282 . . . . . . . . . . . . . . . . 17 (seq1((+g𝐺), (𝐹𝑓)) Fn (ℤ‘1) → dom seq1((+g𝐺), (𝐹𝑓)) = (ℤ‘1))
8683, 84, 85mp2b 10 . . . . . . . . . . . . . . . 16 dom seq1((+g𝐺), (𝐹𝑓)) = (ℤ‘1)
8786eleq2i 2851 . . . . . . . . . . . . . . 15 ((♯‘𝐵) ∈ dom seq1((+g𝐺), (𝐹𝑓)) ↔ (♯‘𝐵) ∈ (ℤ‘1))
8882, 87sylnibr 321 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → ¬ (♯‘𝐵) ∈ dom seq1((+g𝐺), (𝐹𝑓)))
89 ndmfv 6523 . . . . . . . . . . . . . 14 (¬ (♯‘𝐵) ∈ dom seq1((+g𝐺), (𝐹𝑓)) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = ∅)
9088, 89syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = ∅)
91 seqfn 13190 . . . . . . . . . . . . . . . . 17 (1 ∈ ℤ → seq1((+g𝐻), (𝐹𝑓)) Fn (ℤ‘1))
92 fndm 6282 . . . . . . . . . . . . . . . . 17 (seq1((+g𝐻), (𝐹𝑓)) Fn (ℤ‘1) → dom seq1((+g𝐻), (𝐹𝑓)) = (ℤ‘1))
9383, 91, 92mp2b 10 . . . . . . . . . . . . . . . 16 dom seq1((+g𝐻), (𝐹𝑓)) = (ℤ‘1)
9493eleq2i 2851 . . . . . . . . . . . . . . 15 ((♯‘𝐵) ∈ dom seq1((+g𝐻), (𝐹𝑓)) ↔ (♯‘𝐵) ∈ (ℤ‘1))
9582, 94sylnibr 321 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → ¬ (♯‘𝐵) ∈ dom seq1((+g𝐻), (𝐹𝑓)))
96 ndmfv 6523 . . . . . . . . . . . . . 14 (¬ (♯‘𝐵) ∈ dom seq1((+g𝐻), (𝐹𝑓)) → (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)) = ∅)
9795, 96syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)) = ∅)
9890, 97eqtr4d 2811 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))
9998adantlr 702 . . . . . . . . . . 11 (((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) ∧ ¬ (♯‘𝐵) ∈ (ℤ‘1)) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))
10081, 99pm2.61dan 800 . . . . . . . . . 10 ((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐵)) = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))
10144, 100eqtrd 2808 . . . . . . . . 9 ((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)) = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))
102101eqeq2d 2782 . . . . . . . 8 ((𝜑𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)) ↔ 𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵))))
103102pm5.32da 571 . . . . . . 7 (𝜑 → ((𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴))) ↔ (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))
10452f1oeq2d 6434 . . . . . . . . 9 (𝜑 → (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑓:(1...(♯‘𝐵))–1-1-onto𝐴))
10541f1oeq3d 6435 . . . . . . . . 9 (𝜑 → (𝑓:(1...(♯‘𝐵))–1-1-onto𝐴𝑓:(1...(♯‘𝐵))–1-1-onto𝐵))
106104, 105bitrd 271 . . . . . . . 8 (𝜑 → (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑓:(1...(♯‘𝐵))–1-1-onto𝐵))
107106anbi1d 620 . . . . . . 7 (𝜑 → ((𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵))) ↔ (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))
108103, 107bitrd 271 . . . . . 6 (𝜑 → ((𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴))) ↔ (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))
109108exbidv 1880 . . . . 5 (𝜑 → (∃𝑓(𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴))) ↔ ∃𝑓(𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))
110109iotabidv 6167 . . . 4 (𝜑 → (℩𝑥𝑓(𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)))) = (℩𝑥𝑓(𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))
11136, 110ifeq12d 4364 . . 3 (𝜑 → if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴))))) = if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵))))))
11213, 15, 111ifbieq12d 4371 . 2 (𝜑 → if(ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}, (0g𝐺), if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)))))) = if(ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}, (0g𝐻), if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))))
113 eqid 2772 . . 3 (Base‘𝐺) = (Base‘𝐺)
114 eqid 2772 . . 3 (0g𝐺) = (0g𝐺)
115 eqid 2772 . . 3 (+g𝐺) = (+g𝐺)
116 eqid 2772 . . 3 {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}
11739a1i 11 . . 3 (𝜑𝐴 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)})))
118 gsumpropd2.g . . 3 (𝜑𝐺𝑊)
119 gsumpropd2.f . . 3 (𝜑𝐹𝑉)
120 eqidd 2773 . . 3 (𝜑 → dom 𝐹 = dom 𝐹)
121113, 114, 115, 116, 117, 118, 119, 120gsumvalx 17732 . 2 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g𝐺)𝑡) = 𝑡 ∧ (𝑡(+g𝐺)𝑠) = 𝑡)}, (0g𝐺), if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐺), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑥 = (seq1((+g𝐺), (𝐹𝑓))‘(♯‘𝐴)))))))
122 eqid 2772 . . 3 (Base‘𝐻) = (Base‘𝐻)
123 eqid 2772 . . 3 (0g𝐻) = (0g𝐻)
124 eqid 2772 . . 3 (+g𝐻) = (+g𝐻)
125 eqid 2772 . . 3 {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)} = {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}
12640a1i 11 . . 3 (𝜑𝐵 = (𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)})))
127 gsumpropd2.h . . 3 (𝜑𝐻𝑋)
128122, 123, 124, 125, 126, 127, 119, 120gsumvalx 17732 . 2 (𝜑 → (𝐻 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g𝐻)𝑡) = 𝑡 ∧ (𝑡(+g𝐻)𝑠) = 𝑡)}, (0g𝐻), if(dom 𝐹 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝐹 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝐻), 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑥 = (seq1((+g𝐻), (𝐹𝑓))‘(♯‘𝐵)))))))
129112, 121, 1283eqtr4d 2818 1 (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387   = wceq 1507  wex 1742  wcel 2050  wral 3082  wrex 3083  {crab 3086  Vcvv 3409  cdif 3820  wss 3823  c0 4172  ifcif 4344  ccnv 5400  dom cdm 5401  ran crn 5402  cima 5404  ccom 5405  cio 6144  Fun wfun 6176   Fn wfn 6177  wf 6178  1-1-ontowf1o 6181  cfv 6182  (class class class)co 6970  1c1 10330  cz 11787  cuz 12052  ...cfz 12702  seqcseq 13178  chash 13499  Basecbs 16333  +gcplusg 16415  0gc0g 16563   Σg cgsu 16564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7495  df-2nd 7496  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-er 8083  df-en 8301  df-dom 8302  df-sdom 8303  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-nn 11434  df-n0 11702  df-z 11788  df-uz 12053  df-fz 12703  df-seq 13179  df-0g 16565  df-gsum 16566
This theorem is referenced by:  gsumpropd2  17736
  Copyright terms: Public domain W3C validator