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

Theorem frgpuplem 19682
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 19627 . . . . . 6 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))}
4 coeq2 5859 . . . . . . . . . . . . 13 (𝑒 = 𝑣 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝑣))
54oveq2d 7428 . . . . . . . . . . . 12 (𝑒 = 𝑣 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))
6 eqid 2731 . . . . . . . . . . . 12 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} = {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))}
75, 6eqer 8741 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} Er V)
9 ssv 4007 . . . . . . . . . . 11 π‘Š βŠ† V
109a1i 11 . . . . . . . . . 10 (πœ‘ β†’ π‘Š βŠ† V)
118, 10erinxp 8788 . . . . . . . . 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 2767 . . . . . . . . . . 11 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
17 vex 3477 . . . . . . . . . . . . . 14 𝑒 ∈ V
18 vex 3477 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4824 . . . . . . . . . . . . 13 ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ {𝑒, 𝑣} βŠ† π‘Š)
2019anbi1i 623 . . . . . . . . . . . 12 (((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))))
2120opabbii 5216 . . . . . . . . . . 11 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
2216, 21eqtri 2759 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))} ∩ (π‘Š Γ— π‘Š)) = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}
23 ereq1 8713 . . . . . . . . . 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 774 . . . . . . . . . . 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 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o))
32 simprl 768 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Ž ∈ 𝐼)
33 2oconcl 8506 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2o β†’ (1o βˆ– 𝑏) ∈ 2o)
3433ad2antll 726 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (1o βˆ– 𝑏) ∈ 2o)
3532, 34opelxpd 5716 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩ ∈ (𝐼 Γ— 2o))
3631, 35s2cld 14827 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o))
37 splcl 14707 . . . . . . . . . . . . 13 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
3829, 36, 37syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ Word (𝐼 Γ— 2o))
391efgrcl 19625 . . . . . . . . . . . . . 14 (π‘₯ ∈ π‘Š β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
4140simprd 495 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘Š = Word (𝐼 Γ— 2o))
4238, 41eleqtrrd 2835 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)
43 pfxcl 14632 . . . . . . . . . . . . . . . . . 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 19680 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
5251ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑇:(𝐼 Γ— 2o)⟢𝐡)
53 ccatco 14791 . . . . . . . . . . . . . . . . 17 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))
5444, 36, 52, 53syl3anc 1370 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))
5554oveq2d 7428 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
5648ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Grp)
5756grpmndd 18869 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝐻 ∈ Mnd)
58 wrdco 14787 . . . . . . . . . . . . . . . . 17 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
5944, 52, 58syl2anc 583 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡)
60 wrdco 14787 . . . . . . . . . . . . . . . . 17 ((βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
6136, 52, 60syl2anc 583 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡)
62 eqid 2731 . . . . . . . . . . . . . . . . 17 (+gβ€˜π») = (+gβ€˜π»)
6345, 62gsumccat 18759 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡 ∧ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
6457, 59, 61, 63syl3anc 1370 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
6552, 31, 35s2co 14876 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
66 df-ov 7415 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) = (π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
6866fveq2i 6895 . . . . . . . . . . . . . . . . . . . . . 22 (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©))
69 df-ov 7415 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)
70 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
7170efgmval 19622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ (π‘Ž(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)𝑏) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7269, 71eqtr3id 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7372adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©) = βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)
7473fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
7545, 46, 47, 48, 49, 50, 70frgpuptinv 19681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βŸ¨π‘Ž, π‘βŸ© ∈ (𝐼 Γ— 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7630, 75sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7776adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)β€˜βŸ¨π‘Ž, π‘βŸ©)) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7874, 77eqtr3d 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩) = (π‘β€˜(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)))
7968, 78eqtr4id 2790 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) = (π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩))
8067, 79s2eqd 14819 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ© = βŸ¨β€œ(π‘‡β€˜βŸ¨π‘Ž, π‘βŸ©)(π‘‡β€˜βŸ¨π‘Ž, (1o βˆ– 𝑏)⟩)β€βŸ©)
8165, 80eqtr4d 2774 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) = βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©)
8281oveq2d 7428 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©))
83 simprr 770 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑏 ∈ 2o)
8452, 32, 83fovcdmd 7582 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘Žπ‘‡π‘) ∈ 𝐡)
8545, 46grpinvcl 18909 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8656, 84, 85syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡)
8745, 62gsumws2 18760 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (π‘Žπ‘‡π‘) ∈ 𝐡 ∧ (π‘β€˜(π‘Žπ‘‡π‘)) ∈ 𝐡) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
8857, 84, 86, 87syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g βŸ¨β€œ(π‘Žπ‘‡π‘)(π‘β€˜(π‘Žπ‘‡π‘))β€βŸ©) = ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))))
89 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (0gβ€˜π») = (0gβ€˜π»)
9045, 62, 89, 46grprinv 18912 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (π‘Žπ‘‡π‘) ∈ 𝐡) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9156, 84, 90syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘Žπ‘‡π‘)(+gβ€˜π»)(π‘β€˜(π‘Žπ‘‡π‘))) = (0gβ€˜π»))
9282, 88, 913eqtrd 2775 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) = (0gβ€˜π»))
9392oveq2d 7428 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)))
9445gsumwcl 18757 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9557, 59, 94syl2anc 583 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡)
9645, 62, 89grprid 18890 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) ∈ 𝐡) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9756, 95, 96syl2anc 583 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(0gβ€˜π»)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9893, 97eqtrd 2771 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))))
9955, 64, 983eqtrrd 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛))) = (𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©))))
10099oveq1d 7427 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
101 swrdcl 14600 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
10229, 101syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o))
103 wrdco 14787 . . . . . . . . . . . . . . 15 (((π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
104102, 52, 103syl2anc 583 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡)
10545, 62gsumccat 18759 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (π‘₯ prefix 𝑛)) ∈ Word 𝐡 ∧ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
10657, 59, 104, 105syl3anc 1370 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ (π‘₯ prefix 𝑛)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
107 ccatcl 14529 . . . . . . . . . . . . . . . 16 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
10844, 36, 107syl2anc 583 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o))
109 wrdco 14787 . . . . . . . . . . . . . . 15 ((((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
110108, 52, 109syl2anc 583 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡)
11145, 62gsumccat 18759 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ∈ Word 𝐡 ∧ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) ∈ Word 𝐡) β†’ (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
11257, 110, 104, 111syl3anc 1370 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = ((𝐻 Ξ£g (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)))(+gβ€˜π»)(𝐻 Ξ£g (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
113100, 106, 1123eqtr4d 2781 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
114 simplrr 775 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ 𝑛 ∈ (0...(β™―β€˜π‘₯)))
115 lencl 14488 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘₯) ∈ β„•0)
11629, 115syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ β„•0)
117 nn0uz 12869 . . . . . . . . . . . . . . . . . . 19 β„•0 = (β„€β‰₯β€˜0)
118116, 117eleqtrdi 2842 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
119 eluzfz2 13514 . . . . . . . . . . . . . . . . . 18 ((β™―β€˜π‘₯) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
120118, 119syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯)))
121 ccatpfx 14656 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ Word (𝐼 Γ— 2o) ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ (β™―β€˜π‘₯) ∈ (0...(β™―β€˜π‘₯))) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
12229, 114, 120, 121syl3anc 1370 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = (π‘₯ prefix (β™―β€˜π‘₯)))
123 pfxid 14639 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ Word (𝐼 Γ— 2o) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
12429, 123syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ prefix (β™―β€˜π‘₯)) = π‘₯)
125122, 124eqtrd 2771 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)) = π‘₯)
126125coeq2d 5863 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = (𝑇 ∘ π‘₯))
127 ccatco 14791 . . . . . . . . . . . . . . 15 (((π‘₯ prefix 𝑛) ∈ Word (𝐼 Γ— 2o) ∧ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
12844, 102, 52, 127syl3anc 1370 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ ((π‘₯ prefix 𝑛) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
129126, 128eqtr3d 2773 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ π‘₯) = ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
130129oveq2d 7428 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g ((𝑇 ∘ (π‘₯ prefix 𝑛)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
131 splval 14706 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ π‘Š ∧ (𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)) ∧ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) = (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))
13226, 114, 114, 36, 131syl13anc 1371 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) = (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))
133132coeq2d 5863 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
134 ccatco 14791 . . . . . . . . . . . . . . 15 ((((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩) ∈ Word (𝐼 Γ— 2o) ∧ 𝑇:(𝐼 Γ— 2o)⟢𝐡) β†’ (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
135108, 102, 52, 134syl3anc 1370 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©) ++ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
136133, 135eqtrd 2771 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) = ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩))))
137136oveq2d 7428 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))) = (𝐻 Ξ£g ((𝑇 ∘ ((π‘₯ prefix 𝑛) ++ βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©)) ++ (𝑇 ∘ (π‘₯ substr βŸ¨π‘›, (β™―β€˜π‘₯)⟩)))))
138113, 130, 1373eqtr4d 2781 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
139 vex 3477 . . . . . . . . . . . 12 π‘₯ ∈ V
140 ovex 7445 . . . . . . . . . . . 12 (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ V
141 eleq1 2820 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑒 ∈ π‘Š ↔ π‘₯ ∈ π‘Š))
142 eleq1 2820 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑣 ∈ π‘Š ↔ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š))
143141, 142bi2anan9 636 . . . . . . . . . . . . . 14 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ((𝑒 ∈ π‘Š ∧ 𝑣 ∈ π‘Š) ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
14419, 143bitr3id 284 . . . . . . . . . . . . 13 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ (π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š)))
145 coeq2 5859 . . . . . . . . . . . . . . 15 (𝑒 = π‘₯ β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ π‘₯))
146145oveq2d 7428 . . . . . . . . . . . . . 14 (𝑒 = π‘₯ β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ π‘₯)))
147 coeq2 5859 . . . . . . . . . . . . . . 15 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
148147oveq2d 7428 . . . . . . . . . . . . . 14 (𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))
149146, 148eqeqan12d 2745 . . . . . . . . . . . . 13 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ ((𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)) ↔ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))))
150144, 149anbi12d 630 . . . . . . . . . . . 12 ((𝑒 = π‘₯ ∧ 𝑣 = (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)) β†’ (({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣))) ↔ ((π‘₯ ∈ π‘Š ∧ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ∈ π‘Š) ∧ (𝐻 Ξ£g (𝑇 ∘ π‘₯)) = (𝐻 Ξ£g (𝑇 ∘ (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))))))
151 eqid 2731 . . . . . . . . . . . 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 1343 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) ∧ (π‘Ž ∈ 𝐼 ∧ 𝑏 ∈ 2o)) β†’ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
154153ralrimivva 3199 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ π‘Š ∧ 𝑛 ∈ (0...(β™―β€˜π‘₯)))) β†’ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
155154ralrimivva 3199 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©))
1561fvexi 6906 . . . . . . . . . 10 π‘Š ∈ V
157 erex 8730 . . . . . . . . . 10 ({βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š β†’ (π‘Š ∈ V β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V))
15825, 156, 157mpisyl 21 . . . . . . . . 9 (πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} ∈ V)
159 ereq1 8713 . . . . . . . . . . 11 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘Ÿ Er π‘Š ↔ {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} Er π‘Š))
160 breq 5151 . . . . . . . . . . . . 13 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1611602ralbidv 3217 . . . . . . . . . . . 12 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
1621612ralbidv 3217 . . . . . . . . . . 11 (π‘Ÿ = {βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} β†’ (βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯π‘Ÿ(π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©) ↔ βˆ€π‘₯ ∈ π‘Š βˆ€π‘› ∈ (0...(β™―β€˜π‘₯))βˆ€π‘Ž ∈ 𝐼 βˆ€π‘ ∈ 2o π‘₯{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))} (π‘₯ splice βŸ¨π‘›, 𝑛, βŸ¨β€œβŸ¨π‘Ž, π‘βŸ©βŸ¨π‘Ž, (1o βˆ– 𝑏)βŸ©β€βŸ©βŸ©)))
163159, 162anbi12d 630 . . . . . . . . . 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 710 . . . . . . 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 406 . . 3 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ 𝐴{βŸ¨π‘’, π‘£βŸ© ∣ ({𝑒, 𝑣} βŠ† π‘Š ∧ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)))}𝐢)
1721, 2efger 19628 . . . . . 6 ∼ Er π‘Š
173 errel 8715 . . . . . 6 ( ∼ Er π‘Š β†’ Rel ∼ )
174172, 173mp1i 13 . . . . 5 (πœ‘ β†’ Rel ∼ )
175 brrelex12 5729 . . . . 5 ((Rel ∼ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
176174, 175sylan 579 . . . 4 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐴 ∈ V ∧ 𝐢 ∈ V))
177 preq12 4740 . . . . . . 7 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ {𝑒, 𝑣} = {𝐴, 𝐢})
178177sseq1d 4014 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ({𝑒, 𝑣} βŠ† π‘Š ↔ {𝐴, 𝐢} βŠ† π‘Š))
179 coeq2 5859 . . . . . . . 8 (𝑒 = 𝐴 β†’ (𝑇 ∘ 𝑒) = (𝑇 ∘ 𝐴))
180179oveq2d 7428 . . . . . . 7 (𝑒 = 𝐴 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝐴)))
181 coeq2 5859 . . . . . . . 8 (𝑣 = 𝐢 β†’ (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐢))
182181oveq2d 7428 . . . . . . 7 (𝑣 = 𝐢 β†’ (𝐻 Ξ£g (𝑇 ∘ 𝑣)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
183180, 182eqeqan12d 2745 . . . . . 6 ((𝑒 = 𝐴 ∧ 𝑣 = 𝐢) β†’ ((𝐻 Ξ£g (𝑇 ∘ 𝑒)) = (𝐻 Ξ£g (𝑇 ∘ 𝑣)) ↔ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢))))
184178, 183anbi12d 630 . . . . 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 495 1 ((πœ‘ ∧ 𝐴 ∼ 𝐢) β†’ (𝐻 Ξ£g (𝑇 ∘ 𝐴)) = (𝐻 Ξ£g (𝑇 ∘ 𝐢)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {cab 2708  βˆ€wral 3060  Vcvv 3473   βˆ– 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 7412   ∈ cmpo 7414  1oc1o 8462  2oc2o 8463   Er wer 8703  0cc0 11113  β„•0cn0 12477  β„€β‰₯cuz 12827  ...cfz 13489  β™―chash 14295  Word cword 14469   ++ cconcat 14525   substr csubstr 14595   prefix cpfx 14625   splice csplice 14704  βŸ¨β€œcs2 14797  Basecbs 17149  +gcplusg 17202  0gc0g 17390   Ξ£g cgsu 17391  Mndcmnd 18660  Grpcgrp 18856  invgcminusg 18857   ~FG cefg 19616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-2 12280  df-n0 12478  df-z 12564  df-uz 12828  df-fz 13490  df-fzo 13633  df-seq 13972  df-hash 14296  df-word 14470  df-concat 14526  df-s1 14551  df-substr 14596  df-pfx 14626  df-splice 14705  df-s2 14804  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-0g 17392  df-gsum 17393  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-grp 18859  df-minusg 18860  df-efg 19619
This theorem is referenced by:  frgpupf  19683
  Copyright terms: Public domain W3C validator