efgcpbl2 - Metamath Proof Explorer

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

Theorem efgcpbl2 18086

Description: Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_𝑜))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_𝑜 ↦ ⟨𝑦, (1_𝑜 ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2_𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))

**Assertion**
Ref	Expression
efgcpbl2	⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∼ (𝑋 ++ 𝑌))

Distinct variable groups: 𝑦,𝑧 𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥 𝑚,𝑀 𝑥,𝑛,𝑀,𝑡,𝑣,𝑤 𝑘,𝑚,𝑡,𝑥,𝑇 𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥 ∼ ,𝑚,𝑡,𝑥,𝑦,𝑧 𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧 𝐷,𝑚,𝑡 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛) ∼ (𝑤,𝑣,𝑘,𝑛) 𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝑇(𝑦,𝑧,𝑤,𝑣,𝑛) 𝐼(𝑘) 𝑀(𝑦,𝑧,𝑘) 𝑋(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝑌(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)

**Proof of Theorem efgcpbl2**
Step	Hyp	Ref	Expression
1		efgval.w	. . . 4 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2_𝑜))
2		efgval.r	. . . 4 ⊢ ∼ = ( ~_FG ‘𝐼)
3	1, 2	efger 18047	. . 3 ⊢ ∼ Er 𝑊
4	3	a1i 11	. 2 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ∼ Er 𝑊)
5		simpl 473	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐴 ∼ 𝑋)
6	4, 5	ercl 7699	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐴 ∈ 𝑊)
7		wrd0 13264	. . . . 5 ⊢ ∅ ∈ Word (𝐼 × 2_𝑜)
8	1	efgrcl 18044	. . . . . . 7 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2_𝑜)))
9	6, 8	syl 17	. . . . . 6 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2_𝑜)))
10	9	simprd 479	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝑊 = Word (𝐼 × 2_𝑜))
11	7, 10	syl5eleqr 2711	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ∅ ∈ 𝑊)
12		simpr 477	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐵 ∼ 𝑌)
13		efgval2.m	. . . . 5 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_𝑜 ↦ ⟨𝑦, (1_𝑜 ∖ 𝑧)⟩)
14		efgval2.t	. . . . 5 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2_𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
15		efgred.d	. . . . 5 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
16		efgred.s	. . . . 5 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
17	1, 2, 13, 14, 15, 16	efgcpbl 18085	. . . 4 ⊢ ((𝐴 ∈ 𝑊 ∧ ∅ ∈ 𝑊 ∧ 𝐵 ∼ 𝑌) → ((𝐴 ++ 𝐵) ++ ∅) ∼ ((𝐴 ++ 𝑌) ++ ∅))
18	6, 11, 12, 17	syl3anc 1323	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((𝐴 ++ 𝐵) ++ ∅) ∼ ((𝐴 ++ 𝑌) ++ ∅))
19	6, 10	eleqtrd 2706	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐴 ∈ Word (𝐼 × 2_𝑜))
20	4, 12	ercl 7699	. . . . . 6 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐵 ∈ 𝑊)
21	20, 10	eleqtrd 2706	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝐵 ∈ Word (𝐼 × 2_𝑜))
22		ccatcl 13293	. . . . 5 ⊢ ((𝐴 ∈ Word (𝐼 × 2_𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2_𝑜)) → (𝐴 ++ 𝐵) ∈ Word (𝐼 × 2_𝑜))
23	19, 21, 22	syl2anc 692	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∈ Word (𝐼 × 2_𝑜))
24		ccatrid 13304	. . . 4 ⊢ ((𝐴 ++ 𝐵) ∈ Word (𝐼 × 2_𝑜) → ((𝐴 ++ 𝐵) ++ ∅) = (𝐴 ++ 𝐵))
25	23, 24	syl 17	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((𝐴 ++ 𝐵) ++ ∅) = (𝐴 ++ 𝐵))
26	4, 12	ercl2 7701	. . . . . 6 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝑌 ∈ 𝑊)
27	26, 10	eleqtrd 2706	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝑌 ∈ Word (𝐼 × 2_𝑜))
28		ccatcl 13293	. . . . 5 ⊢ ((𝐴 ∈ Word (𝐼 × 2_𝑜) ∧ 𝑌 ∈ Word (𝐼 × 2_𝑜)) → (𝐴 ++ 𝑌) ∈ Word (𝐼 × 2_𝑜))
29	19, 27, 28	syl2anc 692	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝑌) ∈ Word (𝐼 × 2_𝑜))
30		ccatrid 13304	. . . 4 ⊢ ((𝐴 ++ 𝑌) ∈ Word (𝐼 × 2_𝑜) → ((𝐴 ++ 𝑌) ++ ∅) = (𝐴 ++ 𝑌))
31	29, 30	syl 17	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((𝐴 ++ 𝑌) ++ ∅) = (𝐴 ++ 𝑌))
32	18, 25, 31	3brtr3d 4649	. 2 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∼ (𝐴 ++ 𝑌))
33	1, 2, 13, 14, 15, 16	efgcpbl 18085	. . . 4 ⊢ ((∅ ∈ 𝑊 ∧ 𝑌 ∈ 𝑊 ∧ 𝐴 ∼ 𝑋) → ((∅ ++ 𝐴) ++ 𝑌) ∼ ((∅ ++ 𝑋) ++ 𝑌))
34	11, 26, 5, 33	syl3anc 1323	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((∅ ++ 𝐴) ++ 𝑌) ∼ ((∅ ++ 𝑋) ++ 𝑌))
35		ccatlid 13303	. . . . 5 ⊢ (𝐴 ∈ Word (𝐼 × 2_𝑜) → (∅ ++ 𝐴) = 𝐴)
36	19, 35	syl 17	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (∅ ++ 𝐴) = 𝐴)
37	36	oveq1d 6620	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((∅ ++ 𝐴) ++ 𝑌) = (𝐴 ++ 𝑌))
38	4, 5	ercl2 7701	. . . . . 6 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝑋 ∈ 𝑊)
39	38, 10	eleqtrd 2706	. . . . 5 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → 𝑋 ∈ Word (𝐼 × 2_𝑜))
40		ccatlid 13303	. . . . 5 ⊢ (𝑋 ∈ Word (𝐼 × 2_𝑜) → (∅ ++ 𝑋) = 𝑋)
41	39, 40	syl 17	. . . 4 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (∅ ++ 𝑋) = 𝑋)
42	41	oveq1d 6620	. . 3 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → ((∅ ++ 𝑋) ++ 𝑌) = (𝑋 ++ 𝑌))
43	34, 37, 42	3brtr3d 4649	. 2 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝑌) ∼ (𝑋 ++ 𝑌))
44	4, 32, 43	ertrd 7704	1 ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∼ (𝑋 ++ 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1480 ∈ wcel 1992 ∀wral 2912 {crab 2916 Vcvv 3191 ∖ cdif 3557 ∅c0 3896 {csn 4153 ⟨cop 4159 ⟨cotp 4161 ∪ ciun 4490 class class class wbr 4618 ↦ cmpt 4678 I cid 4989 × cxp 5077 ran crn 5080 ‘cfv 5850 (class class class)co 6605 ↦ cmpt2 6607 1_𝑜c1o 7499 2_𝑜c2o 7500 Er wer 7685 0cc0 9881 1c1 9882 − cmin 10211 ...cfz 12265 ..^cfzo 12403 #chash 13054 Word cword 13225 ++ cconcat 13227 splice csplice 13230 ⟨“cs2 13518 ~_FG cefg 18035

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1841 ax-6 1890 ax-7 1937 ax-8 1994 ax-9 2001 ax-10 2021 ax-11 2036 ax-12 2049 ax-13 2250 ax-ext 2606 ax-rep 4736 ax-sep 4746 ax-nul 4754 ax-pow 4808 ax-pr 4872 ax-un 6903 ax-cnex 9937 ax-resscn 9938 ax-1cn 9939 ax-icn 9940 ax-addcl 9941 ax-addrcl 9942 ax-mulcl 9943 ax-mulrcl 9944 ax-mulcom 9945 ax-addass 9946 ax-mulass 9947 ax-distr 9948 ax-i2m1 9949 ax-1ne0 9950 ax-1rid 9951 ax-rnegex 9952 ax-rrecex 9953 ax-cnre 9954 ax-pre-lttri 9955 ax-pre-lttrn 9956 ax-pre-ltadd 9957 ax-pre-mulgt0 9958

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1883 df-eu 2478 df-mo 2479 df-clab 2613 df-cleq 2619 df-clel 2622 df-nfc 2756 df-ne 2797 df-nel 2900 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3193 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3897 df-if 4064 df-pw 4137 df-sn 4154 df-pr 4156 df-tp 4158 df-op 4160 df-ot 4162 df-uni 4408 df-int 4446 df-iun 4492 df-iin 4493 df-br 4619 df-opab 4679 df-mpt 4680 df-tr 4718 df-eprel 4990 df-id 4994 df-po 5000 df-so 5001 df-fr 5038 df-we 5040 df-xp 5085 df-rel 5086 df-cnv 5087 df-co 5088 df-dm 5089 df-rn 5090 df-res 5091 df-ima 5092 df-pred 5642 df-ord 5688 df-on 5689 df-lim 5690 df-suc 5691 df-iota 5813 df-fun 5852 df-fn 5853 df-f 5854 df-f1 5855 df-fo 5856 df-f1o 5857 df-fv 5858 df-riota 6566 df-ov 6608 df-oprab 6609 df-mpt2 6610 df-om 7014 df-1st 7116 df-2nd 7117 df-wrecs 7353 df-recs 7414 df-rdg 7452 df-1o 7506 df-2o 7507 df-oadd 7510 df-er 7688 df-ec 7690 df-map 7805 df-pm 7806 df-en 7901 df-dom 7902 df-sdom 7903 df-fin 7904 df-card 8710 df-pnf 10021 df-mnf 10022 df-xr 10023 df-ltxr 10024 df-le 10025 df-sub 10213 df-neg 10214 df-nn 10966 df-n0 11238 df-z 11323 df-uz 11632 df-fz 12266 df-fzo 12404 df-hash 13055 df-word 13233 df-concat 13235 df-s1 13236 df-substr 13237 df-splice 13238 df-s2 13525 df-efg 18038

This theorem is referenced by: frgpcpbl 18088

W3C validator