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 7 6 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
26 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
27 fex ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐻 ∈ V )
28 16 26 27 sylancl ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 ∈ V )
29 10 28 syl ⊢ ( 𝜑 → 𝐻 ∈ V )
30 f1fun ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → Fun 𝐻 )
31 10 30 syl ⊢ ( 𝜑 → Fun 𝐻 )
32 31 11 jca ⊢ ( 𝜑 → ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) )
33 25 29 32 jca31 ⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
35 imacosupp ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) ) )
36 35 imp ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
37 34 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
38 24 37 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
39 38 f1oeq3d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) ↔ ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ) )
40 23 39 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) )
41 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
42 41 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
43 f1oco ⊢ ( ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
44 40 42 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
45 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
46 frn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 → ran 𝑓 ⊆ 𝑊 )
47 42 45 46 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ran 𝑓 ⊆ 𝑊 )
48 cores ⊢ ( ran 𝑓 ⊆ 𝑊 → ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐻 ∘ 𝑓 ) )
49 f1oeq1 ⊢ ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐻 ∘ 𝑓 ) → ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
50 47 48 49 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( ( 𝐻 ↾ 𝑊 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
51 44 50 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
52 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
53 ssfi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → 𝑊 ∈ Fin )
54 52 20 53 sylancr ⊢ ( 𝜑 → 𝑊 ∈ Fin )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ∈ Fin )
56 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 ) )
57 56 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) )
58 52 a1i ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
59 17 58 fexd ⊢ ( 𝜑 → 𝐻 ∈ V )
60 25 59 32 jca31 ⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) ) )
62 61 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
63 57 62 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
64 63 f1oeq3d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) ↔ ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ) )
65 23 64 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) )
66 55 65 hasheqf1od ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 supp 0 ) ) )
67 66 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
68 67 f1oeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
69 51 68 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) )