Metamath Proof Explorer

Theorem gsumval3lem1

Description: Lemma 1 for gsumval3 . (Contributed by AV, 31-May-2019)

Ref Expression
Hypotheses gsumval3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumval3.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumval3.p ⊢ + = ( +g ‘ 𝐺 )
gsumval3.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumval3.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumval3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumval3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumval3.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumval3.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
gsumval3.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
gsumval3.n ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
gsumval3.w ⊢ 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 )
Assertion gsumval3lem1 ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumval3.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumval3.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumval3.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumval3.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumval3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsumval3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 gsumval3.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumval3.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
10 gsumval3.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
11 gsumval3.n ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
12 gsumval3.w ⊢ 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 )
13 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
14 suppssdm ⊢ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∘ 𝐻 )
15 12 14 eqsstri ⊢ 𝑊 ⊆ dom ( 𝐹 ∘ 𝐻 )
16 f1f ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
17 10 16 syl ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
18 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
19 7 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
20 15 19 fssdm ⊢ ( 𝜑 → 𝑊 ⊆ ( 1 ... 𝑀 ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ⊆ ( 1 ... 𝑀 ) )
22 f1ores ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) )
23 13 21 22 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) )
24 12 imaeq2i ⊢ ( 𝐻 “ 𝑊 ) = ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) )
25 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
26 7 6 25 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
27 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
28 fex ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐻 ∈ V )
29 16 27 28 sylancl ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 ∈ V )
30 10 29 syl ⊢ ( 𝜑 → 𝐻 ∈ V )
31 f1fun ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → Fun 𝐻 )
32 10 31 syl ⊢ ( 𝜑 → Fun 𝐻 )
33 32 11 jca ⊢ ( 𝜑 → ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) )
34 26 30 33 jca31 ⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
35 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
36 imacosupp ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) ) )
37 36 imp ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
38 35 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
39 24 38 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
40 39 f1oeq3d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) ↔ ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ) )
41 23 40 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) )
42 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
43 42 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
44 f1oco ⊢ ( ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
45 41 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
46 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
47 frn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 → ran 𝑓 ⊆ 𝑊 )
48 43 46 47 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ran 𝑓 ⊆ 𝑊 )
49 cores ⊢ ( ran 𝑓 ⊆ 𝑊 → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐻 ∘ 𝑓 ) )
50 f1oeq1 ⊢ ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐻 ∘ 𝑓 ) → ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
51 48 49 50 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
52 45 51 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
53 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
54 ssfi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → 𝑊 ∈ Fin )
55 53 20 54 sylancr ⊢ ( 𝜑 → 𝑊 ∈ Fin )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ∈ Fin )
57 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 ) )
58 57 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) )
59 53 a1i ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
60 fex2 ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ Fin ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V )
61 17 59 6 60 syl3anc ⊢ ( 𝜑 → 𝐻 ∈ V )
62 26 61 33 jca31 ⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
64 63 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
65 58 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
66 65 f1oeq3d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) ↔ ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ) )
67 23 66 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) )
68 56 67 hasheqf1od ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 supp 0 ) ) )
69 68 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
70 69 f1oeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
71 52 70 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) )