Metamath Proof Explorer


Theorem mapfienlem2

Description: Lemma 2 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

Ref Expression
Hypotheses mapfien.s S = x B A | finSupp Z x
mapfien.t T = x D C | finSupp W x
mapfien.w W = G Z
mapfien.f φ F : C 1-1 onto A
mapfien.g φ G : B 1-1 onto D
mapfien.a φ A U
mapfien.b φ B V
mapfien.c φ C X
mapfien.d φ D Y
mapfien.z φ Z B
Assertion mapfienlem2 φ g T finSupp Z G -1 g F -1

Proof

Step Hyp Ref Expression
1 mapfien.s S = x B A | finSupp Z x
2 mapfien.t T = x D C | finSupp W x
3 mapfien.w W = G Z
4 mapfien.f φ F : C 1-1 onto A
5 mapfien.g φ G : B 1-1 onto D
6 mapfien.a φ A U
7 mapfien.b φ B V
8 mapfien.c φ C X
9 mapfien.d φ D Y
10 mapfien.z φ Z B
11 10 adantr φ g T Z B
12 f1of G : B 1-1 onto D G : B D
13 5 12 syl φ G : B D
14 13 10 ffvelrnd φ G Z D
15 3 14 eqeltrid φ W D
16 15 adantr φ g T W D
17 elrabi g x D C | finSupp W x g D C
18 elmapi g D C g : C D
19 17 18 syl g x D C | finSupp W x g : C D
20 19 2 eleq2s g T g : C D
21 20 adantl φ g T g : C D
22 f1ocnv G : B 1-1 onto D G -1 : D 1-1 onto B
23 f1of G -1 : D 1-1 onto B G -1 : D B
24 5 22 23 3syl φ G -1 : D B
25 24 adantr φ g T G -1 : D B
26 ssidd φ g T D D
27 8 adantr φ g T C X
28 9 adantr φ g T D Y
29 breq1 x = g finSupp W x finSupp W g
30 29 elrab g x D C | finSupp W x g D C finSupp W g
31 30 simprbi g x D C | finSupp W x finSupp W g
32 31 2 eleq2s g T finSupp W g
33 32 adantl φ g T finSupp W g
34 5 10 jca φ G : B 1-1 onto D Z B
35 3 eqcomi G Z = W
36 34 35 jctir φ G : B 1-1 onto D Z B G Z = W
37 36 adantr φ g T G : B 1-1 onto D Z B G Z = W
38 f1ocnvfv G : B 1-1 onto D Z B G Z = W G -1 W = Z
39 38 imp G : B 1-1 onto D Z B G Z = W G -1 W = Z
40 37 39 syl φ g T G -1 W = Z
41 11 16 21 25 26 27 28 33 40 fsuppcor φ g T finSupp Z G -1 g
42 f1ocnv F : C 1-1 onto A F -1 : A 1-1 onto C
43 f1of1 F -1 : A 1-1 onto C F -1 : A 1-1 C
44 4 42 43 3syl φ F -1 : A 1-1 C
45 44 adantr φ g T F -1 : A 1-1 C
46 13 7 jca φ G : B D B V
47 fex G : B D B V G V
48 cnvexg G V G -1 V
49 46 47 48 3syl φ G -1 V
50 coexg G -1 V g T G -1 g V
51 49 50 sylan φ g T G -1 g V
52 41 45 11 51 fsuppco φ g T finSupp Z G -1 g F -1