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

Theorem frgpuplem 19561
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 19506 . . . . . 6 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))}
4 coeq2 5819 . . . . . . . . . . . . 13 (𝑒 = 𝑣 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝑣))
54oveq2d 7378 . . . . . . . . . . . 12 (𝑒 = 𝑣 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))
6 eqid 2737 . . . . . . . . . . . 12 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} = {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}
75, 6eqer 8690 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V)
9 ssv 3973 . . . . . . . . . . 11 π‘Š βŠ† V
109a1i 11 . . . . . . . . . 10 (πœ‘ β†’ π‘Š βŠ† V)
118, 10erinxp 8737 . . . . . . . . 9 (πœ‘ β†’ ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) Er π‘Š)
12 df-xp 5644 . . . . . . . . . . . . 13 (π‘Š Γ— π‘Š) = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)}
1312ineq1i 4173 . . . . . . . . . . . 12 ((π‘Š Γ— π‘Š) ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = ({βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)} ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))})
14 incom 4166 . . . . . . . . . . . 12 ((π‘Š Γ— π‘Š) ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š))
15 inopab 5790 . . . . . . . . . . . 12 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š)} ∩ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}) = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
1613, 14, 153eqtr3i 2773 . . . . . . . . . . 11 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
17 vex 3452 . . . . . . . . . . . . . 14 𝑒 ∈ V
18 vex 3452 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4785 . . . . . . . . . . . . 13 ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ {𝑒, 𝑣} βŠ† π‘Š)
2019anbi1i 625 . . . . . . . . . . . 12 (((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))))
2120opabbii 5177 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
2216, 21eqtri 2765 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
23 ereq1 8662 . . . . . . . . . 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 6923 . . . . . . . . . . . . . . 15 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
281, 27eqsstri 3983 . . . . . . . . . . . . . 14 π‘Š βŠ† Word (𝐼 Γ— 2o)
2928, 26sselid 3947 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯ ∈ Word (𝐼 Γ— 2o))
30 opelxpi 5675 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o))
3130adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o))
32 simprl 770 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Ž ∈ 𝐼)
33 2oconcl 8454 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2o β†’ (1o βˆ– 𝑏) ∈ 2o)
3433ad2antll 728 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (1o βˆ– 𝑏) ∈ 2o)
3532, 34opelxpd 5676 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩ ∈ (𝐼 Γ— 2o))
3631, 35s2cld 14767 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o))
37 splcl 14647 . . . . . . . . . . . . 13 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
3829, 36, 37syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
391efgrcl 19504 . . . . . . . . . . . . . 14 (π‘₯ ∈ π‘Š β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4140simprd 497 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Š = Word (𝐼 Γ— 2o))
4238, 41eleqtrrd 2841 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)
43 pfxcl 14572 . . . . . . . . . . . . . . . . . 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 19559 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
5251ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
53 ccatco 14731 . . . . . . . . . . . . . . . . 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 7378 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
5648ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Grp)
5756grpmndd 18767 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Mnd)
58 wrdco 14727 . . . . . . . . . . . . . . . . 17 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
5944, 52, 58syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
60 wrdco 14727 . . . . . . . . . . . . . . . . 17 ((βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
6136, 52, 60syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
62 eqid 2737 . . . . . . . . . . . . . . . . 17 (+gβ€˜π») = (+gβ€˜π»)
6345, 62gsumccat 18658 . . . . . . . . . . . . . . . 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 14816 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
66 df-ov 7365 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
6866fveq2i 6850 . . . . . . . . . . . . . . . . . . . . . 22 (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
69 df-ov 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)
70 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
7170efgmval 19501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7269, 71eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7372adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7473fveq2d 6851 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
7545, 46, 47, 48, 49, 50, 70frgpuptinv 19560 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7630, 75sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7776adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7874, 77eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7968, 78eqtr4id 2796 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
8067, 79s2eqd 14759 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ© = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
8165, 80eqtr4d 2780 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©)
8281oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©))
83 simprr 772 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑏 ∈ 2o)
8452, 32, 83fovcdmd 7531 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) ∈ 𝐡)
8545, 46grpinvcl 18805 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8656, 84, 85syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8745, 62gsumws2 18659 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (π‘Žπ‘‡π‘) ∈ 𝐡 ∧ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
8857, 84, 86, 87syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
89 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (0gβ€˜π») = (0gβ€˜π»)
9045, 62, 89, 46grprinv 18808 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9156, 84, 90syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9282, 88, 913eqtrd 2781 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (0gβ€˜π»))
9392oveq2d 7378 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)))
9445gsumwcl 18656 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9557, 59, 94syl2anc 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9645, 62, 89grprid 18788 . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9955, 64, 983eqtrrd 2782 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) = (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
10099oveq1d 7377 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
101 swrdcl 14540 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
10229, 101syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
103 wrdco 14727 . . . . . . . . . . . . . . 15 (((π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
104102, 52, 103syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
10545, 62gsumccat 18658 . . . . . . . . . . . . . 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 14469 . . . . . . . . . . . . . . . 16 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
10844, 36, 107syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
109 wrdco 14727 . . . . . . . . . . . . . . 15 ((((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
110108, 52, 109syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
11145, 62gsumccat 18658 . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
114 simplrr 777 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑛 ∈ (0...(β™―β€˜π‘₯)))
115 lencl 14428 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘₯) ∈ β„•0)
11629, 115syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ β„•0)
117 nn0uz 12812 . . . . . . . . . . . . . . . . . . 19 β„•0 = (β„€β‰₯β€˜0)
118116, 117eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
119 eluzfz2 13456 . . . . . . . . . . . . . . . . . 18 ((β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
120118, 119syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
121 ccatpfx 14596 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯))) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
12229, 114, 120, 121syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
123 pfxid 14579 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
12429, 123syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
125122, 124eqtrd 2777 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = π‘₯)
126125coeq2d 5823 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = (𝑇 ∘ π‘₯))
127 ccatco 14731 . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ π‘₯) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
130129oveq2d 7378 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
131 splval 14646 . . . . . . . . . . . . . . . 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 5823 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
134 ccatco 14731 . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
137136oveq2d 7378 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
138113, 130, 1373eqtr4d 2787 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
139 vex 3452 . . . . . . . . . . . 12 π‘₯ ∈ V
140 ovex 7395 . . . . . . . . . . . 12 (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ V
141 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑒 ∈ π‘Š ↔ π‘₯ ∈ π‘Š))
142 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑣 ∈ π‘Š ↔ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š))
143141, 142bi2anan9 638 . . . . . . . . . . . . . 14 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
14419, 143bitr3id 285 . . . . . . . . . . . . 13 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
145 coeq2 5819 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ π‘₯))
146145oveq2d 7378 . . . . . . . . . . . . . 14 (𝑒 = π‘₯ β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ π‘₯)))
147 coeq2 5819 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
148147oveq2d 7378 . . . . . . . . . . . . . 14 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
149146, 148eqeqan12d 2751 . . . . . . . . . . . . 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 2737 . . . . . . . . . . . 12 {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
152139, 140, 150, 151braba 5499 . . . . . . . . . . 11 (π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ ((π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))))
15326, 42, 138, 152syl21anbrc 1345 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
154153ralrimivva 3198 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) β†’ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
155154ralrimivva 3198 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
1561fvexi 6861 . . . . . . . . . 10 π‘Š ∈ V
157 erex 8679 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š β†’ (π‘Š ∈ V β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V))
15825, 156, 157mpisyl 21 . . . . . . . . 9 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V)
159 ereq1 8662 . . . . . . . . . . 11 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘Ÿ Er π‘Š ↔ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š))
160 breq 5112 . . . . . . . . . . . . 13 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1611602ralbidv 3213 . . . . . . . . . . . 12 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1621612ralbidv 3213 . . . . . . . . . . 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 3633 . . . . . . . . 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 4929 . . . . . . 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 3997 . . . . 5 (πœ‘ β†’ ∼ βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))})
170169ssbrd 5153 . . . 4 (πœ‘ β†’ (𝐴 ∼ 𝐢 β†’ 𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢))
171170imp 408 . . 3 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ 𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢)
1721, 2efger 19507 . . . . . 6 ∼ Er π‘Š
173 errel 8664 . . . . . 6 ( ∼ Er π‘Š β†’ Rel ∼ )
174172, 173mp1i 13 . . . . 5 (πœ‘ β†’ Rel ∼ )
175 brrelex12 5689 . . . . 5 ((Rel ∼ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
176174, 175sylan 581 . . . 4 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
177 preq12 4701 . . . . . . 7 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ {𝑒, 𝑣} = {𝐴, 𝐢})
178177sseq1d 3980 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ {𝐴, 𝐢} βŠ† π‘Š))
179 coeq2 5819 . . . . . . . 8 (𝑒 = 𝐴 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝐴))
180179oveq2d 7378 . . . . . . 7 (𝑒 = 𝐴 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝐴)))
181 coeq2 5819 . . . . . . . 8 (𝑣 = 𝐢 β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐢))
182181oveq2d 7378 . . . . . . 7 (𝑣 = 𝐢 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
183180, 182eqeqan12d 2751 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ((𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)) ↔ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢))))
184178, 183anbi12d 632 . . . . 5 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ (({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ({𝐴, 𝐢} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))))
185184, 151brabga 5496 . . . 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 2714  βˆ€wral 3065  Vcvv 3448   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {cpr 4593  βŸ¨cop 4597  βŸ¨cotp 4599  βˆ© cint 4912   class class class wbr 5110  {copab 5172   I cid 5535   Γ— cxp 5636   ∘ ccom 5642  Rel wrel 5643  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364  1oc1o 8410  2oc2o 8411   Er wer 8652  0cc0 11058  β„•0cn0 12420  β„€β‰₯cuz 12770  ...cfz 13431  β™―chash 14237  Word cword 14409   ++ cconcat 14465   substr csubstr 14535   prefix cpfx 14565   splice csplice 14644  βŸ¨β€œcs2 14737  Basecbs 17090  +gcplusg 17140  0gc0g 17328   Ξ£g cgsu 17329  Mndcmnd 18563  Grpcgrp 18755  invgcminusg 18756   ~FG cefg 19495
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-ot 4600  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-n0 12421  df-z 12507  df-uz 12771  df-fz 13432  df-fzo 13575  df-seq 13914  df-hash 14238  df-word 14410  df-concat 14466  df-s1 14491  df-substr 14536  df-pfx 14566  df-splice 14645  df-s2 14744  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-0g 17330  df-gsum 17331  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-grp 18758  df-minusg 18759  df-efg 19498
This theorem is referenced by:  frgpupf  19562
  Copyright terms: Public domain W3C validator