Metamath Proof Explorer

Theorem gsmsymgreq

Description: Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
Assertion gsmsymgreq ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left({W}\in \mathrm{Word}{B}\wedge {U}\in \mathrm{Word}{P}\wedge \left|{W}\right|=\left|{U}\right|\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
2 gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
4 gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
5 gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
6 fveq2 ${⊢}{w}=\varnothing \to \left|{w}\right|=\left|\varnothing \right|$
7 6 oveq2d ${⊢}{w}=\varnothing \to \left(0..^\left|{w}\right|\right)=\left(0..^\left|\varnothing \right|\right)$
8 7 adantr ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|\varnothing \right|\right)$
9 fveq1 ${⊢}{w}=\varnothing \to {w}\left({i}\right)=\varnothing \left({i}\right)$
10 9 fveq1d ${⊢}{w}=\varnothing \to {w}\left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)$
11 fveq1 ${⊢}{u}=\varnothing \to {u}\left({i}\right)=\varnothing \left({i}\right)$
12 11 fveq1d ${⊢}{u}=\varnothing \to {u}\left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)$
13 10 12 eqeqan12d ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left({w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\right)$
14 13 ralbidv ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\right)$
15 8 14 raleqbidv ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|\varnothing \right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\right)$
16 oveq2 ${⊢}{w}=\varnothing \to {\sum }_{{S}}{w}={\sum }_{{S}}\varnothing$
17 16 fveq1d ${⊢}{w}=\varnothing \to \left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{S}},\varnothing \right)\left({n}\right)$
18 oveq2 ${⊢}{u}=\varnothing \to {\sum }_{{Z}}{u}={\sum }_{{Z}}\varnothing$
19 18 fveq1d ${⊢}{u}=\varnothing \to \left({\sum }_{{Z}},{u}\right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)$
20 17 19 eqeqan12d ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)\right)$
21 20 ralbidv ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)\right)$
22 15 21 imbi12d ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|\varnothing \right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)\right)\right)$
23 22 imbi2d ${⊢}\left({w}=\varnothing \wedge {u}=\varnothing \right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|\varnothing \right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)\right)\right)\right)$
24 fveq2 ${⊢}{w}={x}\to \left|{w}\right|=\left|{x}\right|$
25 24 oveq2d ${⊢}{w}={x}\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|{x}\right|\right)$
26 25 adantr ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|{x}\right|\right)$
27 fveq1 ${⊢}{w}={x}\to {w}\left({i}\right)={x}\left({i}\right)$
28 27 fveq1d ${⊢}{w}={x}\to {w}\left({i}\right)\left({n}\right)={x}\left({i}\right)\left({n}\right)$
29 fveq1 ${⊢}{u}={y}\to {u}\left({i}\right)={y}\left({i}\right)$
30 29 fveq1d ${⊢}{u}={y}\to {u}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)$
31 28 30 eqeqan12d ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left({w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\right)$
32 31 ralbidv ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\right)$
33 26 32 raleqbidv ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\right)$
34 oveq2 ${⊢}{w}={x}\to {\sum }_{{S}}{w}={\sum }_{{S}}{x}$
35 34 fveq1d ${⊢}{w}={x}\to \left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{S}},{x}\right)\left({n}\right)$
36 oveq2 ${⊢}{u}={y}\to {\sum }_{{Z}}{u}={\sum }_{{Z}}{y}$
37 36 fveq1d ${⊢}{u}={y}\to \left({\sum }_{{Z}},{u}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)$
38 35 37 eqeqan12d ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)$
39 38 ralbidv ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)$
40 33 39 imbi12d ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)\right)$
41 40 imbi2d ${⊢}\left({w}={x}\wedge {u}={y}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)\right)\right)$
42 fveq2 ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to \left|{w}\right|=\left|{x}\mathrm{++}⟨“{b}”⟩\right|$
43 42 oveq2d ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)$
44 43 adantr ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)$
45 fveq1 ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to {w}\left({i}\right)=\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)$
46 45 fveq1d ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to {w}\left({i}\right)\left({n}\right)=\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)$
47 fveq1 ${⊢}{u}={y}\mathrm{++}⟨“{p}”⟩\to {u}\left({i}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)$
48 47 fveq1d ${⊢}{u}={y}\mathrm{++}⟨“{p}”⟩\to {u}\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)$
49 46 48 eqeqan12d ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left({w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\right)$
50 49 ralbidv ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\right)$
51 44 50 raleqbidv ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\right)$
52 oveq2 ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to {\sum }_{{S}}{w}={\sum }_{{S}}\left({x}\mathrm{++}⟨“{b}”⟩\right)$
53 52 fveq1d ${⊢}{w}={x}\mathrm{++}⟨“{b}”⟩\to \left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)$
54 oveq2 ${⊢}{u}={y}\mathrm{++}⟨“{p}”⟩\to {\sum }_{{Z}}{u}={\sum }_{{Z}}\left({y}\mathrm{++}⟨“{p}”⟩\right)$
55 54 fveq1d ${⊢}{u}={y}\mathrm{++}⟨“{p}”⟩\to \left({\sum }_{{Z}},{u}\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)$
56 53 55 eqeqan12d ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)$
57 56 ralbidv ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)$
58 51 57 imbi12d ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)\right)$
59 58 imbi2d ${⊢}\left({w}={x}\mathrm{++}⟨“{b}”⟩\wedge {u}={y}\mathrm{++}⟨“{p}”⟩\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)\right)\right)$
60 fveq2 ${⊢}{w}={W}\to \left|{w}\right|=\left|{W}\right|$
61 60 oveq2d ${⊢}{w}={W}\to \left(0..^\left|{w}\right|\right)=\left(0..^\left|{W}\right|\right)$
62 fveq1 ${⊢}{w}={W}\to {w}\left({i}\right)={W}\left({i}\right)$
63 62 fveq1d ${⊢}{w}={W}\to {w}\left({i}\right)\left({n}\right)={W}\left({i}\right)\left({n}\right)$
64 63 eqeq1d ${⊢}{w}={W}\to \left({w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)↔{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
65 64 ralbidv ${⊢}{w}={W}\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
66 61 65 raleqbidv ${⊢}{w}={W}\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
67 oveq2 ${⊢}{w}={W}\to {\sum }_{{S}}{w}={\sum }_{{S}}{W}$
68 67 fveq1d ${⊢}{w}={W}\to \left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{S}},{W}\right)\left({n}\right)$
69 68 eqeq1d ${⊢}{w}={W}\to \left(\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)↔\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$
70 69 ralbidv ${⊢}{w}={W}\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$
71 66 70 imbi12d ${⊢}{w}={W}\to \left(\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)$
72 71 imbi2d ${⊢}{w}={W}\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)\right)$
73 fveq1 ${⊢}{u}={U}\to {u}\left({i}\right)={U}\left({i}\right)$
74 73 fveq1d ${⊢}{u}={U}\to {u}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)$
75 74 eqeq2d ${⊢}{u}={U}\to \left({w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
76 75 ralbidv ${⊢}{u}={U}\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
77 76 ralbidv ${⊢}{u}={U}\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\right)$
78 oveq2 ${⊢}{u}={U}\to {\sum }_{{Z}}{u}={\sum }_{{Z}}{U}$
79 78 fveq1d ${⊢}{u}={U}\to \left({\sum }_{{Z}},{u}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)$
80 79 eqeq2d ${⊢}{u}={U}\to \left(\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$
81 80 ralbidv ${⊢}{u}={U}\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$
82 77 81 imbi12d ${⊢}{u}={U}\to \left(\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)$
83 82 imbi2d ${⊢}{u}={U}\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={u}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{u}\right)\left({n}\right)\right)\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{w}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{w}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{w}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)\right)$
84 eleq2 ${⊢}{I}={N}\cap {M}\to \left({n}\in {I}↔{n}\in \left({N}\cap {M}\right)\right)$
85 elin ${⊢}{n}\in \left({N}\cap {M}\right)↔\left({n}\in {N}\wedge {n}\in {M}\right)$
86 84 85 syl6bb ${⊢}{I}={N}\cap {M}\to \left({n}\in {I}↔\left({n}\in {N}\wedge {n}\in {M}\right)\right)$
87 simpl ${⊢}\left({n}\in {N}\wedge {n}\in {M}\right)\to {n}\in {N}$
88 86 87 syl6bi ${⊢}{I}={N}\cap {M}\to \left({n}\in {I}\to {n}\in {N}\right)$
89 5 88 ax-mp ${⊢}{n}\in {I}\to {n}\in {N}$
90 89 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge {n}\in {I}\right)\to {n}\in {N}$
91 fvresi ${⊢}{n}\in {N}\to \left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)={n}$
92 90 91 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge {n}\in {I}\right)\to \left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)={n}$
93 simpr ${⊢}\left({n}\in {N}\wedge {n}\in {M}\right)\to {n}\in {M}$
94 86 93 syl6bi ${⊢}{I}={N}\cap {M}\to \left({n}\in {I}\to {n}\in {M}\right)$
95 5 94 ax-mp ${⊢}{n}\in {I}\to {n}\in {M}$
96 95 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge {n}\in {I}\right)\to {n}\in {M}$
97 fvresi ${⊢}{n}\in {M}\to \left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)={n}$
98 96 97 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge {n}\in {I}\right)\to \left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)={n}$
99 92 98 eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge {n}\in {I}\right)\to \left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)=\left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)$
100 99 ralrimiva ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)=\left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)$
101 1 symgid ${⊢}{N}\in \mathrm{Fin}\to {\mathrm{I}↾}_{{N}}={0}_{{S}}$
102 101 adantr ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to {\mathrm{I}↾}_{{N}}={0}_{{S}}$
103 eqid ${⊢}{0}_{{S}}={0}_{{S}}$
104 103 gsum0 ${⊢}{\sum }_{{S}}\varnothing ={0}_{{S}}$
105 102 104 syl6reqr ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to {\sum }_{{S}}\varnothing ={\mathrm{I}↾}_{{N}}$
106 105 fveq1d ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)$
107 3 symgid ${⊢}{M}\in \mathrm{Fin}\to {\mathrm{I}↾}_{{M}}={0}_{{Z}}$
108 107 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to {\mathrm{I}↾}_{{M}}={0}_{{Z}}$
109 eqid ${⊢}{0}_{{Z}}={0}_{{Z}}$
110 109 gsum0 ${⊢}{\sum }_{{Z}}\varnothing ={0}_{{Z}}$
111 108 110 syl6reqr ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to {\sum }_{{Z}}\varnothing ={\mathrm{I}↾}_{{M}}$
112 111 fveq1d ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left({\sum }_{{Z}},\varnothing \right)\left({n}\right)=\left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)$
113 106 112 eqeq12d ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)↔\left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)=\left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)\right)$
114 113 ralbidv ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{{N}}\right)\left({n}\right)=\left({\mathrm{I}↾}_{{M}}\right)\left({n}\right)\right)$
115 100 114 mpbird ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)$
116 115 a1d ${⊢}\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|\varnothing \right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\varnothing \left({i}\right)\left({n}\right)=\varnothing \left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\varnothing \right)\left({n}\right)=\left({\sum }_{{Z}},\varnothing \right)\left({n}\right)\right)$
117 1 2 3 4 5 gsmsymgreqlem2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({x}\in \mathrm{Word}{B}\wedge {b}\in {B}\right)\wedge \left({y}\in \mathrm{Word}{P}\wedge {p}\in {P}\right)\wedge \left|{x}\right|=\left|{y}\right|\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)\right)$
118 117 expcom ${⊢}\left(\left({x}\in \mathrm{Word}{B}\wedge {b}\in {B}\right)\wedge \left({y}\in \mathrm{Word}{P}\wedge {p}\in {P}\right)\wedge \left|{x}\right|=\left|{y}\right|\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\left(\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)\right)\right)$
119 118 a2d ${⊢}\left(\left({x}\in \mathrm{Word}{B}\wedge {b}\in {B}\right)\wedge \left({y}\in \mathrm{Word}{P}\wedge {p}\in {P}\right)\wedge \left|{x}\right|=\left|{y}\right|\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{x}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)\left({n}\right)={y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{x}\right)\left({n}\right)=\left({\sum }_{{Z}},{y}\right)\left({n}\right)\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{x}\mathrm{++}⟨“{b}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{++}⟨“{b}”⟩\right)\left({i}\right)\left({n}\right)=\left({y}\mathrm{++}⟨“{p}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({x}\mathrm{++}⟨“{b}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({y}\mathrm{++}⟨“{p}”⟩\right)\right)\left({n}\right)\right)\right)\right)$
120 23 41 59 72 83 116 119 wrd2ind ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {U}\in \mathrm{Word}{P}\wedge \left|{W}\right|=\left|{U}\right|\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)\right)$
121 120 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left({W}\in \mathrm{Word}{B}\wedge {U}\in \mathrm{Word}{P}\wedge \left|{W}\right|=\left|{U}\right|\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({n}\right)={U}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{W}\right)\left({n}\right)=\left({\sum }_{{Z}},{U}\right)\left({n}\right)\right)$