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

Theorem frgpuplem 19640
Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
frgpup.b 𝐡 = (Baseβ€˜π»)
frgpup.n 𝑁 = (invgβ€˜π»)
frgpup.t 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = βˆ…, (πΉβ€˜π‘¦), (π‘β€˜(πΉβ€˜π‘¦))))
frgpup.h (πœ‘ β†’ 𝐻 ∈ Grp)
frgpup.i (πœ‘ β†’ 𝐼 ∈ 𝑉)
frgpup.a (πœ‘ β†’ 𝐹:𝐼⟢𝐡)
frgpup.w π‘Š = ( I β€˜Word (𝐼 Γ— 2o))
frgpup.r ∼ = ( ~FG β€˜πΌ)
Assertion
Ref Expression
frgpuplem ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐹,𝑧   𝑦,𝑁,𝑧   𝑦,𝐡,𝑧   πœ‘,𝑦,𝑧   𝑦,𝐼,𝑧
Allowed substitution hints:   𝐢(𝑦,𝑧)   ∼ (𝑦,𝑧)   𝑇(𝑦,𝑧)   𝐻(𝑦,𝑧)   𝑉(𝑦,𝑧)   π‘Š(𝑦,𝑧)

Proof of Theorem frgpuplem
Dummy variables π‘Ž 𝑏 𝑒 𝑣 𝑛 π‘Ÿ π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpup.w . . . . . . 7 π‘Š = ( I β€˜Word (𝐼 Γ— 2o))
2 frgpup.r . . . . . . 7 ∼ = ( ~FG β€˜πΌ)
31, 2efgval 19585 . . . . . 6 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))}
4 coeq2 5859 . . . . . . . . . . . . 13 (𝑒 = 𝑣 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝑣))
54oveq2d 7425 . . . . . . . . . . . 12 (𝑒 = 𝑣 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))
6 eqid 2733 . . . . . . . . . . . 12 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} = {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}
75, 6eqer 8738 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V)
9 ssv 4007 . . . . . . . . . . 11 π‘Š βŠ† V
109a1i 11 . . . . . . . . . 10 (πœ‘ β†’ π‘Š βŠ† V)
118, 10erinxp 8785 . . . . . . . . 9 (πœ‘ β†’ ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) Er π‘Š)
12 df-xp 5683 . . . . . . . . . . . . 13 (π‘Š Γ— π‘Š) = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)}
1312ineq1i 4209 . . . . . . . . . . . 12 ((π‘Š Γ— π‘Š) ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = ({βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)} ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))})
14 incom 4202 . . . . . . . . . . . 12 ((π‘Š Γ— π‘Š) ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š))
15 inopab 5830 . . . . . . . . . . . 12 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)} ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
1613, 14, 153eqtr3i 2769 . . . . . . . . . . 11 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
17 vex 3479 . . . . . . . . . . . . . 14 𝑒 ∈ V
18 vex 3479 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4824 . . . . . . . . . . . . 13 ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ {𝑒, 𝑣} βŠ† π‘Š)
2019anbi1i 625 . . . . . . . . . . . 12 (((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))))
2120opabbii 5216 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
2216, 21eqtri 2761 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
23 ereq1 8710 . . . . . . . . . 10 (({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) Er π‘Š ↔ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š))
2422, 23ax-mp 5 . . . . . . . . 9 (({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) Er π‘Š ↔ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š)
2511, 24sylib 217 . . . . . . . 8 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š)
26 simplrl 776 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯ ∈ π‘Š)
27 fviss 6969 . . . . . . . . . . . . . . 15 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
281, 27eqsstri 4017 . . . . . . . . . . . . . 14 π‘Š βŠ† Word (𝐼 Γ— 2o)
2928, 26sselid 3981 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯ ∈ Word (𝐼 Γ— 2o))
30 opelxpi 5714 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o))
3130adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o))
32 simprl 770 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Ž ∈ 𝐼)
33 2oconcl 8503 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2o β†’ (1o βˆ– 𝑏) ∈ 2o)
3433ad2antll 728 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (1o βˆ– 𝑏) ∈ 2o)
3532, 34opelxpd 5716 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩ ∈ (𝐼 Γ— 2o))
3631, 35s2cld 14822 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o))
37 splcl 14702 . . . . . . . . . . . . 13 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
3829, 36, 37syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
391efgrcl 19583 . . . . . . . . . . . . . 14 (π‘₯ ∈ π‘Š β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4140simprd 497 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Š = Word (𝐼 Γ— 2o))
4238, 41eleqtrrd 2837 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)
43 pfxcl 14627 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o))
4429, 43syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o))
45 frgpup.b . . . . . . . . . . . . . . . . . . 19 𝐡 = (Baseβ€˜π»)
46 frgpup.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (invgβ€˜π»)
47 frgpup.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = βˆ…, (πΉβ€˜π‘¦), (π‘β€˜(πΉβ€˜π‘¦))))
48 frgpup.h . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐻 ∈ Grp)
49 frgpup.i . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐼 ∈ 𝑉)
50 frgpup.a . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹:𝐼⟢𝐡)
5145, 46, 47, 48, 49, 50frgpuptf 19638 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
5251ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
53 ccatco 14786 . . . . . . . . . . . . . . . . 17 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))
5444, 36, 52, 53syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))
5554oveq2d 7425 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
5648ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Grp)
5756grpmndd 18832 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Mnd)
58 wrdco 14782 . . . . . . . . . . . . . . . . 17 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
5944, 52, 58syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
60 wrdco 14782 . . . . . . . . . . . . . . . . 17 ((βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
6136, 52, 60syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
62 eqid 2733 . . . . . . . . . . . . . . . . 17 (+gβ€˜π») = (+gβ€˜π»)
6345, 62gsumccat 18722 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡 ∧ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
6457, 59, 61, 63syl3anc 1372 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
6552, 31, 35s2co 14871 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
66 df-ov 7412 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
6866fveq2i 6895 . . . . . . . . . . . . . . . . . . . . . 22 (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
69 df-ov 7412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)
70 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
7170efgmval 19580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7269, 71eqtr3id 2787 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7372adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7473fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
7545, 46, 47, 48, 49, 50, 70frgpuptinv 19639 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7630, 75sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7776adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7874, 77eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7968, 78eqtr4id 2792 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
8067, 79s2eqd 14814 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ© = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
8165, 80eqtr4d 2776 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©)
8281oveq2d 7425 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©))
83 simprr 772 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑏 ∈ 2o)
8452, 32, 83fovcdmd 7579 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) ∈ 𝐡)
8545, 46grpinvcl 18872 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8656, 84, 85syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8745, 62gsumws2 18723 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (π‘Žπ‘‡π‘) ∈ 𝐡 ∧ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
8857, 84, 86, 87syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
89 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (0gβ€˜π») = (0gβ€˜π»)
9045, 62, 89, 46grprinv 18875 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9156, 84, 90syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9282, 88, 913eqtrd 2777 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (0gβ€˜π»))
9392oveq2d 7425 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)))
9445gsumwcl 18720 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9557, 59, 94syl2anc 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9645, 62, 89grprid 18853 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9756, 95, 96syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9893, 97eqtrd 2773 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9955, 64, 983eqtrrd 2778 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) = (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
10099oveq1d 7424 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
101 swrdcl 14595 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
10229, 101syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
103 wrdco 14782 . . . . . . . . . . . . . . 15 (((π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
104102, 52, 103syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
10545, 62gsumccat 18722 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡 ∧ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
10657, 59, 104, 105syl3anc 1372 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
107 ccatcl 14524 . . . . . . . . . . . . . . . 16 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
10844, 36, 107syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
109 wrdco 14782 . . . . . . . . . . . . . . 15 ((((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
110108, 52, 109syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
11145, 62gsumccat 18722 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡 ∧ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
11257, 110, 104, 111syl3anc 1372 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
113100, 106, 1123eqtr4d 2783 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
114 simplrr 777 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑛 ∈ (0...(β™―β€˜π‘₯)))
115 lencl 14483 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘₯) ∈ β„•0)
11629, 115syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ β„•0)
117 nn0uz 12864 . . . . . . . . . . . . . . . . . . 19 β„•0 = (β„€β‰₯β€˜0)
118116, 117eleqtrdi 2844 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
119 eluzfz2 13509 . . . . . . . . . . . . . . . . . 18 ((β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
120118, 119syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
121 ccatpfx 14651 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯))) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
12229, 114, 120, 121syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
123 pfxid 14634 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
12429, 123syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
125122, 124eqtrd 2773 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = π‘₯)
126125coeq2d 5863 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = (𝑇 ∘ π‘₯))
127 ccatco 14786 . . . . . . . . . . . . . . 15 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
12844, 102, 52, 127syl3anc 1372 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
129126, 128eqtr3d 2775 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ π‘₯) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
130129oveq2d 7425 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
131 splval 14701 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ π‘Š ∧ (𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) = (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))
13226, 114, 114, 36, 131syl13anc 1373 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) = (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))
133132coeq2d 5863 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
134 ccatco 14786 . . . . . . . . . . . . . . 15 ((((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
135108, 102, 52, 134syl3anc 1372 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
136133, 135eqtrd 2773 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
137136oveq2d 7425 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
138113, 130, 1373eqtr4d 2783 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
139 vex 3479 . . . . . . . . . . . 12 π‘₯ ∈ V
140 ovex 7442 . . . . . . . . . . . 12 (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ V
141 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑒 ∈ π‘Š ↔ π‘₯ ∈ π‘Š))
142 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑣 ∈ π‘Š ↔ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š))
143141, 142bi2anan9 638 . . . . . . . . . . . . . 14 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
14419, 143bitr3id 285 . . . . . . . . . . . . 13 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
145 coeq2 5859 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ π‘₯))
146145oveq2d 7425 . . . . . . . . . . . . . 14 (𝑒 = π‘₯ β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ π‘₯)))
147 coeq2 5859 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
148147oveq2d 7425 . . . . . . . . . . . . . 14 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
149146, 148eqeqan12d 2747 . . . . . . . . . . . . 13 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ((𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)) ↔ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))))
150144, 149anbi12d 632 . . . . . . . . . . . 12 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ (({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ((π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))))
151 eqid 2733 . . . . . . . . . . . 12 {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
152139, 140, 150, 151braba 5538 . . . . . . . . . . 11 (π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ ((π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))))
15326, 42, 138, 152syl21anbrc 1345 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
154153ralrimivva 3201 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) β†’ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
155154ralrimivva 3201 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
1561fvexi 6906 . . . . . . . . . 10 π‘Š ∈ V
157 erex 8727 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š β†’ (π‘Š ∈ V β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V))
15825, 156, 157mpisyl 21 . . . . . . . . 9 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V)
159 ereq1 8710 . . . . . . . . . . 11 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘Ÿ Er π‘Š ↔ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š))
160 breq 5151 . . . . . . . . . . . . 13 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1611602ralbidv 3219 . . . . . . . . . . . 12 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1621612ralbidv 3219 . . . . . . . . . . 11 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
163159, 162anbi12d 632 . . . . . . . . . 10 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ ((π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) ↔ ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
164163elabg 3667 . . . . . . . . 9 ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V β†’ ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))} ↔ ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
165158, 164syl 17 . . . . . . . 8 (πœ‘ β†’ ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))} ↔ ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
16625, 155, 165mpbir2and 712 . . . . . . 7 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))})
167 intss1 4968 . . . . . . 7 ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))} β†’ ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))} βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))})
168166, 167syl 17 . . . . . 6 (πœ‘ β†’ ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))} βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))})
1693, 168eqsstrid 4031 . . . . 5 (πœ‘ β†’ ∼ βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))})
170169ssbrd 5192 . . . 4 (πœ‘ β†’ (𝐴 ∼ 𝐢 β†’ 𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢))
171170imp 408 . . 3 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ 𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢)
1721, 2efger 19586 . . . . . 6 ∼ Er π‘Š
173 errel 8712 . . . . . 6 ( ∼ Er π‘Š β†’ Rel ∼ )
174172, 173mp1i 13 . . . . 5 (πœ‘ β†’ Rel ∼ )
175 brrelex12 5729 . . . . 5 ((Rel ∼ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
176174, 175sylan 581 . . . 4 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
177 preq12 4740 . . . . . . 7 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ {𝑒, 𝑣} = {𝐴, 𝐢})
178177sseq1d 4014 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ {𝐴, 𝐢} βŠ† π‘Š))
179 coeq2 5859 . . . . . . . 8 (𝑒 = 𝐴 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝐴))
180179oveq2d 7425 . . . . . . 7 (𝑒 = 𝐴 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝐴)))
181 coeq2 5859 . . . . . . . 8 (𝑣 = 𝐢 β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐢))
182181oveq2d 7425 . . . . . . 7 (𝑣 = 𝐢 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
183180, 182eqeqan12d 2747 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ((𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)) ↔ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢))))
184178, 183anbi12d 632 . . . . 5 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ (({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ({𝐴, 𝐢} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))))
185184, 151brabga 5535 . . . 4 ((𝐴 ∈ V ∧ 𝐢 ∈ V) β†’ (𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢 ↔ ({𝐴, 𝐢} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))))
186176, 185syl 17 . . 3 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢 ↔ ({𝐴, 𝐢} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))))
187171, 186mpbid 231 . 2 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ ({𝐴, 𝐢} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢))))
188187simprd 497 1 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  Vcvv 3475   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529  {cpr 4631  βŸ¨cop 4635  βŸ¨cotp 4637  βˆ© cint 4951   class class class wbr 5149  {copab 5211   I cid 5574   Γ— cxp 5675   ∘ ccom 5681  Rel wrel 5682  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1oc1o 8459  2oc2o 8460   Er wer 8700  0cc0 11110  β„•0cn0 12472  β„€β‰₯cuz 12822  ...cfz 13484  β™―chash 14290  Word cword 14464   ++ cconcat 14520   substr csubstr 14590   prefix cpfx 14620   splice csplice 14699  βŸ¨β€œcs2 14792  Basecbs 17144  +gcplusg 17197  0gc0g 17385   Ξ£g cgsu 17386  Mndcmnd 18625  Grpcgrp 18819  invgcminusg 18820   ~FG cefg 19574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-word 14465  df-concat 14521  df-s1 14546  df-substr 14591  df-pfx 14621  df-splice 14700  df-s2 14799  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-0g 17387  df-gsum 17388  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-grp 18822  df-minusg 18823  df-efg 19577
This theorem is referenced by:  frgpupf  19641
  Copyright terms: Public domain W3C validator