Metamath Proof Explorer

Theorem swrdccat3blem

Description: Lemma for swrdccat3b . (Contributed by AV, 30-May-2018)

Ref Expression
Hypothesis swrdccatin2.l ⊢L=A
Assertion swrdccat3blem ⊢A∈WordV∧B∈WordV∧M∈0…L+B∧L+B≤L→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢L=A
2 lencl ⊢B∈WordV→B∈ℕ0
3 nn0le0eq0 ⊢B∈ℕ0→B≤0↔B=0
4 3 biimpd ⊢B∈ℕ0→B≤0→B=0
5 2 4 syl ⊢B∈WordV→B≤0→B=0
6 5 adantl ⊢A∈WordV∧B∈WordV→B≤0→B=0
7 hasheq0 ⊢B∈WordV→B=0↔B=∅
8 7 biimpd ⊢B∈WordV→B=0→B=∅
9 8 adantl ⊢A∈WordV∧B∈WordV→B=0→B=∅
10 9 imp ⊢A∈WordV∧B∈WordV∧B=0→B=∅
11 lencl ⊢A∈WordV→A∈ℕ0
12 1 eqcomi ⊢A=L
13 12 eleq1i ⊢A∈ℕ0↔L∈ℕ0
14 nn0re ⊢L∈ℕ0→L∈ℝ
15 elfz2nn0 ⊢M∈0…L+0↔M∈ℕ0∧L+0∈ℕ0∧M≤L+0
16 recn ⊢L∈ℝ→L∈ℂ
17 16 addridd ⊢L∈ℝ→L+0=L
18 17 breq2d ⊢L∈ℝ→M≤L+0↔M≤L
19 nn0re ⊢M∈ℕ0→M∈ℝ
20 19 anim1i ⊢M∈ℕ0∧L∈ℝ→M∈ℝ∧L∈ℝ
21 20 ancoms ⊢L∈ℝ∧M∈ℕ0→M∈ℝ∧L∈ℝ
22 letri3 ⊢M∈ℝ∧L∈ℝ→M=L↔M≤L∧L≤M
23 21 22 syl ⊢L∈ℝ∧M∈ℕ0→M=L↔M≤L∧L≤M
24 23 biimprd ⊢L∈ℝ∧M∈ℕ0→M≤L∧L≤M→M=L
25 24 exp4b ⊢L∈ℝ→M∈ℕ0→M≤L→L≤M→M=L
26 25 com23 ⊢L∈ℝ→M≤L→M∈ℕ0→L≤M→M=L
27 18 26 sylbid ⊢L∈ℝ→M≤L+0→M∈ℕ0→L≤M→M=L
28 27 com3l ⊢M≤L+0→M∈ℕ0→L∈ℝ→L≤M→M=L
29 28 impcom ⊢M∈ℕ0∧M≤L+0→L∈ℝ→L≤M→M=L
30 29 3adant2 ⊢M∈ℕ0∧L+0∈ℕ0∧M≤L+0→L∈ℝ→L≤M→M=L
31 30 com12 ⊢L∈ℝ→M∈ℕ0∧L+0∈ℕ0∧M≤L+0→L≤M→M=L
32 15 31 biimtrid ⊢L∈ℝ→M∈0…L+0→L≤M→M=L
33 14 32 syl ⊢L∈ℕ0→M∈0…L+0→L≤M→M=L
34 13 33 sylbi ⊢A∈ℕ0→M∈0…L+0→L≤M→M=L
35 11 34 syl ⊢A∈WordV→M∈0…L+0→L≤M→M=L
36 35 imp ⊢A∈WordV∧M∈0…L+0→L≤M→M=L
37 elfznn0 ⊢M∈0…L+0→M∈ℕ0
38 swrd00 ⊢∅substr00=∅
39 swrd00 ⊢AsubstrLL=∅
40 38 39 eqtr4i ⊢∅substr00=AsubstrLL
41 nn0cn ⊢L∈ℕ0→L∈ℂ
42 41 subidd ⊢L∈ℕ0→L−L=0
43 42 opeq1d ⊢L∈ℕ0→L−L0=00
44 43 oveq2d ⊢L∈ℕ0→∅substrL−L0=∅substr00
45 41 addridd ⊢L∈ℕ0→L+0=L
46 45 opeq2d ⊢L∈ℕ0→LL+0=LL
47 46 oveq2d ⊢L∈ℕ0→AsubstrLL+0=AsubstrLL
48 40 44 47 3eqtr4a ⊢L∈ℕ0→∅substrL−L0=AsubstrLL+0
49 48 a1i ⊢M=L→L∈ℕ0→∅substrL−L0=AsubstrLL+0
50 eleq1 ⊢M=L→M∈ℕ0↔L∈ℕ0
51 oveq1 ⊢M=L→M−L=L−L
52 51 opeq1d ⊢M=L→M−L0=L−L0
53 52 oveq2d ⊢M=L→∅substrM−L0=∅substrL−L0
54 opeq1 ⊢M=L→ML+0=LL+0
55 54 oveq2d ⊢M=L→AsubstrML+0=AsubstrLL+0
56 53 55 eqeq12d ⊢M=L→∅substrM−L0=AsubstrML+0↔∅substrL−L0=AsubstrLL+0
57 49 50 56 3imtr4d ⊢M=L→M∈ℕ0→∅substrM−L0=AsubstrML+0
58 57 com12 ⊢M∈ℕ0→M=L→∅substrM−L0=AsubstrML+0
59 58 a1d ⊢M∈ℕ0→A∈WordV→M=L→∅substrM−L0=AsubstrML+0
60 37 59 syl ⊢M∈0…L+0→A∈WordV→M=L→∅substrM−L0=AsubstrML+0
61 60 impcom ⊢A∈WordV∧M∈0…L+0→M=L→∅substrM−L0=AsubstrML+0
62 36 61 syld ⊢A∈WordV∧M∈0…L+0→L≤M→∅substrM−L0=AsubstrML+0
63 62 imp ⊢A∈WordV∧M∈0…L+0∧L≤M→∅substrM−L0=AsubstrML+0
64 swrdcl ⊢A∈WordV→AsubstrML∈WordV
65 ccatrid ⊢AsubstrML∈WordV→AsubstrML++∅=AsubstrML
66 64 65 syl ⊢A∈WordV→AsubstrML++∅=AsubstrML
67 13 41 sylbi ⊢A∈ℕ0→L∈ℂ
68 11 67 syl ⊢A∈WordV→L∈ℂ
69 addrid ⊢L∈ℂ→L+0=L
70 69 eqcomd ⊢L∈ℂ→L=L+0
71 68 70 syl ⊢A∈WordV→L=L+0
72 71 opeq2d ⊢A∈WordV→ML=ML+0
73 72 oveq2d ⊢A∈WordV→AsubstrML=AsubstrML+0
74 66 73 eqtrd ⊢A∈WordV→AsubstrML++∅=AsubstrML+0
75 74 adantr ⊢A∈WordV∧M∈0…L+0→AsubstrML++∅=AsubstrML+0
76 75 adantr ⊢A∈WordV∧M∈0…L+0∧¬L≤M→AsubstrML++∅=AsubstrML+0
77 63 76 ifeqda ⊢A∈WordV∧M∈0…L+0→ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
78 77 ex ⊢A∈WordV→M∈0…L+0→ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
79 78 ad3antrrr ⊢A∈WordV∧B∈WordV∧B=0∧B=∅→M∈0…L+0→ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
80 oveq2 ⊢B=0→L+B=L+0
81 80 oveq2d ⊢B=0→0…L+B=0…L+0
82 81 eleq2d ⊢B=0→M∈0…L+B↔M∈0…L+0
83 82 adantr ⊢B=0∧B=∅→M∈0…L+B↔M∈0…L+0
84 simpr ⊢B=0∧B=∅→B=∅
85 opeq2 ⊢B=0→M−LB=M−L0
86 85 adantr ⊢B=0∧B=∅→M−LB=M−L0
87 84 86 oveq12d ⊢B=0∧B=∅→BsubstrM−LB=∅substrM−L0
88 oveq2 ⊢B=∅→AsubstrML++B=AsubstrML++∅
89 88 adantl ⊢B=0∧B=∅→AsubstrML++B=AsubstrML++∅
90 87 89 ifeq12d ⊢B=0∧B=∅→ifL≤MBsubstrM−LBAsubstrML++B=ifL≤M∅substrM−L0AsubstrML++∅
91 80 opeq2d ⊢B=0→ML+B=ML+0
92 91 oveq2d ⊢B=0→AsubstrML+B=AsubstrML+0
93 92 adantr ⊢B=0∧B=∅→AsubstrML+B=AsubstrML+0
94 90 93 eqeq12d ⊢B=0∧B=∅→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B↔ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
95 83 94 imbi12d ⊢B=0∧B=∅→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B↔M∈0…L+0→ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
96 95 adantll ⊢A∈WordV∧B∈WordV∧B=0∧B=∅→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B↔M∈0…L+0→ifL≤M∅substrM−L0AsubstrML++∅=AsubstrML+0
97 79 96 mpbird ⊢A∈WordV∧B∈WordV∧B=0∧B=∅→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
98 10 97 mpdan ⊢A∈WordV∧B∈WordV∧B=0→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
99 98 ex ⊢A∈WordV∧B∈WordV→B=0→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
100 6 99 syld ⊢A∈WordV∧B∈WordV→B≤0→M∈0…L+B→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
101 100 com23 ⊢A∈WordV∧B∈WordV→M∈0…L+B→B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
102 101 imp ⊢A∈WordV∧B∈WordV∧M∈0…L+B→B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
103 102 adantr ⊢A∈WordV∧B∈WordV∧M∈0…L+B∧L+B≤L→B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
104 1 eleq1i ⊢L∈ℕ0↔A∈ℕ0
105 104 14 sylbir ⊢A∈ℕ0→L∈ℝ
106 11 105 syl ⊢A∈WordV→L∈ℝ
107 2 nn0red ⊢B∈WordV→B∈ℝ
108 leaddle0 ⊢L∈ℝ∧B∈ℝ→L+B≤L↔B≤0
109 106 107 108 syl2an ⊢A∈WordV∧B∈WordV→L+B≤L↔B≤0
110 pm2.24 ⊢B≤0→¬B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
111 109 110 syl6bi ⊢A∈WordV∧B∈WordV→L+B≤L→¬B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
112 111 adantr ⊢A∈WordV∧B∈WordV∧M∈0…L+B→L+B≤L→¬B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
113 112 imp ⊢A∈WordV∧B∈WordV∧M∈0…L+B∧L+B≤L→¬B≤0→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B
114 103 113 pm2.61d ⊢A∈WordV∧B∈WordV∧M∈0…L+B∧L+B≤L→ifL≤MBsubstrM−LBAsubstrML++B=AsubstrML+B