Step |
Hyp |
Ref |
Expression |
1 |
|
cyc3conja.c |
⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 3 } ) ) |
2 |
|
cyc3conja.a |
⊢ 𝐴 = ( pmEven ‘ 𝐷 ) |
3 |
|
cyc3conja.s |
⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) |
4 |
|
cyc3conja.n |
⊢ 𝑁 = ( ♯ ‘ 𝐷 ) |
5 |
|
cyc3conja.m |
⊢ 𝑀 = ( toCyc ‘ 𝐷 ) |
6 |
|
cyc3conja.p |
⊢ + = ( +g ‘ 𝑆 ) |
7 |
|
cyc3conja.l |
⊢ − = ( -g ‘ 𝑆 ) |
8 |
|
cyc3conja.1 |
⊢ ( 𝜑 → 5 ≤ 𝑁 ) |
9 |
|
cyc3conja.d |
⊢ ( 𝜑 → 𝐷 ∈ Fin ) |
10 |
|
cyc3conja.q |
⊢ ( 𝜑 → 𝑄 ∈ 𝐶 ) |
11 |
|
cyc3conja.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝐶 ) |
12 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ 𝐴 ) |
13 |
|
simpr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑝 = 𝑔 ) → 𝑝 = 𝑔 ) |
14 |
13
|
oveq1d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑝 = 𝑔 ) → ( 𝑝 + 𝑇 ) = ( 𝑔 + 𝑇 ) ) |
15 |
14 13
|
oveq12d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑝 = 𝑔 ) → ( ( 𝑝 + 𝑇 ) − 𝑝 ) = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
16 |
15
|
eqeq2d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑝 = 𝑔 ) → ( 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ↔ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ) |
17 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
18 |
12 16 17
|
rspcedvd |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ 𝑔 ∈ 𝐴 ) → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |
19 |
9
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝐷 ∈ Fin ) |
20 |
19
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐷 ∈ Fin ) |
21 |
|
simp-8r |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑔 ∈ ( Base ‘ 𝑆 ) ) |
22 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ 𝑔 ∈ 𝐴 ) |
23 |
21 22
|
eldifd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑔 ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ) |
24 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) |
25 |
24
|
eldifad |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐷 ) |
26 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) |
27 |
26
|
eldifad |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐷 ) |
28 |
25 27
|
prssd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 ) |
29 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 ) |
30 |
|
pr2nelem |
⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o ) |
31 |
24 26 29 30
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o ) |
32 |
|
eqid |
⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 ) |
33 |
|
eqid |
⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 ) |
34 |
32 33
|
pmtrrn |
⊢ ( ( 𝐷 ∈ Fin ∧ { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ { 𝑥 , 𝑦 } ≈ 2o ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) |
35 |
20 28 31 34
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) |
36 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
37 |
3 36 33
|
pmtrodpm |
⊢ ( ( 𝐷 ∈ Fin ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) ) ) |
38 |
20 35 37
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) ) ) |
39 |
2
|
difeq2i |
⊢ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) = ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) ) |
40 |
38 39
|
eleqtrrdi |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ) |
41 |
3 36 2
|
odpmco |
⊢ ( ( 𝐷 ∈ Fin ∧ 𝑔 ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ 𝐴 ) |
42 |
20 23 40 41
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ 𝐴 ) |
43 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
44 |
43
|
oveq1d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( 𝑝 + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ) |
45 |
44 43
|
oveq12d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( ( 𝑝 + 𝑇 ) − 𝑝 ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) − ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
46 |
45
|
eqeq2d |
⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ↔ 𝑄 = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) − ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) ) |
47 |
38
|
eldifad |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) |
48 |
|
0zd |
⊢ ( 𝜑 → 0 ∈ ℤ ) |
49 |
|
hashcl |
⊢ ( 𝐷 ∈ Fin → ( ♯ ‘ 𝐷 ) ∈ ℕ0 ) |
50 |
9 49
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℕ0 ) |
51 |
4 50
|
eqeltrid |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
52 |
51
|
nn0zd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
53 |
|
3z |
⊢ 3 ∈ ℤ |
54 |
53
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℤ ) |
55 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
56 |
54
|
zred |
⊢ ( 𝜑 → 3 ∈ ℝ ) |
57 |
|
3pos |
⊢ 0 < 3 |
58 |
57
|
a1i |
⊢ ( 𝜑 → 0 < 3 ) |
59 |
55 56 58
|
ltled |
⊢ ( 𝜑 → 0 ≤ 3 ) |
60 |
|
5re |
⊢ 5 ∈ ℝ |
61 |
60
|
a1i |
⊢ ( 𝜑 → 5 ∈ ℝ ) |
62 |
51
|
nn0red |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
63 |
|
3lt5 |
⊢ 3 < 5 |
64 |
63
|
a1i |
⊢ ( 𝜑 → 3 < 5 ) |
65 |
56 61 64
|
ltled |
⊢ ( 𝜑 → 3 ≤ 5 ) |
66 |
56 61 62 65 8
|
letrd |
⊢ ( 𝜑 → 3 ≤ 𝑁 ) |
67 |
48 52 54 59 66
|
elfzd |
⊢ ( 𝜑 → 3 ∈ ( 0 ... 𝑁 ) ) |
68 |
1 3 4 5 36
|
cycpmgcl |
⊢ ( ( 𝐷 ∈ Fin ∧ 3 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ ( Base ‘ 𝑆 ) ) |
69 |
9 67 68
|
syl2anc |
⊢ ( 𝜑 → 𝐶 ⊆ ( Base ‘ 𝑆 ) ) |
70 |
69 11
|
sseldd |
⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝑆 ) ) |
71 |
70
|
ad8antr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑇 ∈ ( Base ‘ 𝑆 ) ) |
72 |
5 20 25 27 29 32
|
cycpm2tr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) |
73 |
72
|
reseq1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ran 𝑢 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ↾ ran 𝑢 ) ) |
74 |
25 27
|
s2cld |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 〈“ 𝑥 𝑦 ”〉 ∈ Word 𝐷 ) |
75 |
25 27 29
|
s2f1 |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 〈“ 𝑥 𝑦 ”〉 : dom 〈“ 𝑥 𝑦 ”〉 –1-1→ 𝐷 ) |
76 |
5 20 74 75
|
tocycfvres2 |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) = ( I ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) ) |
77 |
76
|
reseq1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) ↾ ran 𝑢 ) = ( ( I ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) ↾ ran 𝑢 ) ) |
78 |
|
simplr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) |
79 |
78
|
elin1d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) |
80 |
|
id |
⊢ ( 𝑤 = 𝑢 → 𝑤 = 𝑢 ) |
81 |
|
dmeq |
⊢ ( 𝑤 = 𝑢 → dom 𝑤 = dom 𝑢 ) |
82 |
|
eqidd |
⊢ ( 𝑤 = 𝑢 → 𝐷 = 𝐷 ) |
83 |
80 81 82
|
f1eq123d |
⊢ ( 𝑤 = 𝑢 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) ) |
84 |
83
|
elrab |
⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) ) |
85 |
79 84
|
sylib |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) ) |
86 |
85
|
simprd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 ) |
87 |
|
f1f |
⊢ ( 𝑢 : dom 𝑢 –1-1→ 𝐷 → 𝑢 : dom 𝑢 ⟶ 𝐷 ) |
88 |
|
frn |
⊢ ( 𝑢 : dom 𝑢 ⟶ 𝐷 → ran 𝑢 ⊆ 𝐷 ) |
89 |
86 87 88
|
3syl |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ran 𝑢 ⊆ 𝐷 ) |
90 |
89
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ran 𝑢 ⊆ 𝐷 ) |
91 |
24 26
|
prssd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) ) |
92 |
|
ssconb |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷 ) → ( { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) ↔ ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) ) ) |
93 |
92
|
biimpa |
⊢ ( ( ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷 ) ∧ { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) ) → ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) ) |
94 |
28 90 91 93
|
syl21anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) ) |
95 |
24 26
|
s2rn |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ran 〈“ 𝑥 𝑦 ”〉 = { 𝑥 , 𝑦 } ) |
96 |
95
|
difeq2d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) = ( 𝐷 ∖ { 𝑥 , 𝑦 } ) ) |
97 |
94 96
|
sseqtrrd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ran 𝑢 ⊆ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) |
98 |
97
|
resabs1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) ↾ ran 𝑢 ) = ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ran 𝑢 ) ) |
99 |
97
|
resabs1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( I ↾ ( 𝐷 ∖ ran 〈“ 𝑥 𝑦 ”〉 ) ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) ) |
100 |
77 98 99
|
3eqtr3d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑀 ‘ 〈“ 𝑥 𝑦 ”〉 ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) ) |
101 |
73 100
|
eqtr3d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) ) |
102 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑀 ‘ 𝑢 ) = 𝑇 ) |
103 |
102
|
reseq1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( 𝑇 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) |
104 |
85
|
simpld |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑢 ∈ Word 𝐷 ) |
105 |
104
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑢 ∈ Word 𝐷 ) |
106 |
86
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 ) |
107 |
5 20 105 106
|
tocycfvres2 |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) |
108 |
103 107
|
eqtr3d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑇 ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) |
109 |
|
disjdif |
⊢ ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ |
110 |
109
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ ) |
111 |
|
undif |
⊢ ( ran 𝑢 ⊆ 𝐷 ↔ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 ) |
112 |
90 111
|
sylib |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 ) |
113 |
3 36 47 71 101 108 110 112
|
symgcom |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) = ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
114 |
113
|
coeq2d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
115 |
3 36 6
|
symgov |
⊢ ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
116 |
21 47 115
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
117 |
3 36 6
|
symgcl |
⊢ ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ) |
118 |
21 47 117
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ) |
119 |
116 118
|
eqeltrrd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ) |
120 |
3 36 6
|
symgov |
⊢ ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) ) |
121 |
119 71 120
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) ) |
122 |
|
coass |
⊢ ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) = ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) ) |
123 |
121 122
|
eqtrdi |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) ) ) |
124 |
|
coass |
⊢ ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
125 |
124
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
126 |
114 123 125
|
3eqtr4d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
127 |
|
cnvco |
⊢ ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) |
128 |
127
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) ) |
129 |
126 128
|
coeq12d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) ) ) |
130 |
|
coass |
⊢ ( ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ◡ 𝑔 ) = ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) ) |
131 |
|
coass |
⊢ ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) |
132 |
131
|
coeq1i |
⊢ ( ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ◡ 𝑔 ) = ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ ◡ 𝑔 ) |
133 |
130 132
|
eqtr3i |
⊢ ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) ) = ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ ◡ 𝑔 ) |
134 |
133
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ 𝑔 ) ) = ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ ◡ 𝑔 ) ) |
135 |
3 36 6
|
symgov |
⊢ ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + 𝑇 ) = ( 𝑔 ∘ 𝑇 ) ) |
136 |
21 71 135
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 + 𝑇 ) = ( 𝑔 ∘ 𝑇 ) ) |
137 |
3 36 6
|
symgcl |
⊢ ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ) |
138 |
21 71 137
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ) |
139 |
136 138
|
eqeltrrd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑔 ∘ 𝑇 ) ∈ ( Base ‘ 𝑆 ) ) |
140 |
3 36
|
symgbasf |
⊢ ( ( 𝑔 ∘ 𝑇 ) ∈ ( Base ‘ 𝑆 ) → ( 𝑔 ∘ 𝑇 ) : 𝐷 ⟶ 𝐷 ) |
141 |
|
fcoi1 |
⊢ ( ( 𝑔 ∘ 𝑇 ) : 𝐷 ⟶ 𝐷 → ( ( 𝑔 ∘ 𝑇 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑔 ∘ 𝑇 ) ) |
142 |
139 140 141
|
3syl |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ 𝑇 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑔 ∘ 𝑇 ) ) |
143 |
3 36
|
elsymgbas |
⊢ ( 𝐷 ∈ Fin → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ↔ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷 –1-1-onto→ 𝐷 ) ) |
144 |
143
|
biimpa |
⊢ ( ( 𝐷 ∈ Fin ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷 –1-1-onto→ 𝐷 ) |
145 |
20 47 144
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷 –1-1-onto→ 𝐷 ) |
146 |
|
f1ococnv2 |
⊢ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷 –1-1-onto→ 𝐷 → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( I ↾ 𝐷 ) ) |
147 |
145 146
|
syl |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( I ↾ 𝐷 ) ) |
148 |
147
|
coeq2d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( 𝑔 ∘ 𝑇 ) ∘ ( I ↾ 𝐷 ) ) ) |
149 |
142 148 136
|
3eqtr4d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( 𝑔 + 𝑇 ) ) |
150 |
149
|
coeq1d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ ◡ 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ ◡ 𝑔 ) ) |
151 |
3 36 7
|
symgsubg |
⊢ ( ( ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 + 𝑇 ) − 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ ◡ 𝑔 ) ) |
152 |
138 21 151
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 + 𝑇 ) − 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ ◡ 𝑔 ) ) |
153 |
150 152
|
eqtr4d |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ 𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ◡ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ ◡ 𝑔 ) = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
154 |
129 134 153
|
3eqtrd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
155 |
3
|
symggrp |
⊢ ( 𝐷 ∈ Fin → 𝑆 ∈ Grp ) |
156 |
9 155
|
syl |
⊢ ( 𝜑 → 𝑆 ∈ Grp ) |
157 |
156
|
ad8antr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑆 ∈ Grp ) |
158 |
36 6
|
grpcl |
⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ) |
159 |
157 119 71 158
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ) |
160 |
3 36 7
|
symgsubg |
⊢ ( ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) − ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
161 |
159 119 160
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) − ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ◡ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
162 |
|
simp-7r |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
163 |
154 161 162
|
3eqtr4rd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑄 = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) − ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) |
164 |
42 46 163
|
rspcedvd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |
165 |
9
|
difexd |
⊢ ( 𝜑 → ( 𝐷 ∖ ran 𝑢 ) ∈ V ) |
166 |
165
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( 𝐷 ∖ ran 𝑢 ) ∈ V ) |
167 |
|
3p2e5 |
⊢ ( 3 + 2 ) = 5 |
168 |
167 8
|
eqbrtrid |
⊢ ( 𝜑 → ( 3 + 2 ) ≤ 𝑁 ) |
169 |
|
2re |
⊢ 2 ∈ ℝ |
170 |
169
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ ) |
171 |
56 170 62
|
leaddsub2d |
⊢ ( 𝜑 → ( ( 3 + 2 ) ≤ 𝑁 ↔ 2 ≤ ( 𝑁 − 3 ) ) ) |
172 |
168 171
|
mpbid |
⊢ ( 𝜑 → 2 ≤ ( 𝑁 − 3 ) ) |
173 |
172
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 2 ≤ ( 𝑁 − 3 ) ) |
174 |
4
|
a1i |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑁 = ( ♯ ‘ 𝐷 ) ) |
175 |
78
|
elin2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 𝑢 ∈ ( ◡ ♯ “ { 3 } ) ) |
176 |
|
hashf |
⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) |
177 |
|
ffn |
⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V ) |
178 |
|
fniniseg |
⊢ ( ♯ Fn V → ( 𝑢 ∈ ( ◡ ♯ “ { 3 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 3 ) ) ) |
179 |
176 177 178
|
mp2b |
⊢ ( 𝑢 ∈ ( ◡ ♯ “ { 3 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 3 ) ) |
180 |
179
|
simprbi |
⊢ ( 𝑢 ∈ ( ◡ ♯ “ { 3 } ) → ( ♯ ‘ 𝑢 ) = 3 ) |
181 |
175 180
|
syl |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( ♯ ‘ 𝑢 ) = 3 ) |
182 |
|
vex |
⊢ 𝑢 ∈ V |
183 |
182
|
dmex |
⊢ dom 𝑢 ∈ V |
184 |
|
hashf1rn |
⊢ ( ( dom 𝑢 ∈ V ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) ) |
185 |
183 86 184
|
sylancr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) ) |
186 |
181 185
|
eqtr3d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 3 = ( ♯ ‘ ran 𝑢 ) ) |
187 |
174 186
|
oveq12d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( 𝑁 − 3 ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) ) |
188 |
173 187
|
breqtrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 2 ≤ ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) ) |
189 |
|
hashssdif |
⊢ ( ( 𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) ) |
190 |
19 89 189
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) ) |
191 |
188 190
|
breqtrrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → 2 ≤ ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) ) |
192 |
|
hashge2el2dif |
⊢ ( ( ( 𝐷 ∖ ran 𝑢 ) ∈ V ∧ 2 ≤ ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) ) → ∃ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∃ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) 𝑥 ≠ 𝑦 ) |
193 |
166 191 192
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ∃ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∃ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) 𝑥 ≠ 𝑦 ) |
194 |
164 193
|
r19.29vva |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑇 ) → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |
195 |
|
nfcv |
⊢ Ⅎ 𝑢 𝑀 |
196 |
5 3 36
|
tocycf |
⊢ ( 𝐷 ∈ Fin → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) ) |
197 |
|
ffn |
⊢ ( 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) |
198 |
9 196 197
|
3syl |
⊢ ( 𝜑 → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) |
199 |
11 1
|
eleqtrdi |
⊢ ( 𝜑 → 𝑇 ∈ ( 𝑀 “ ( ◡ ♯ “ { 3 } ) ) ) |
200 |
195 198 199
|
fvelimad |
⊢ ( 𝜑 → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ( 𝑀 ‘ 𝑢 ) = 𝑇 ) |
201 |
200
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 3 } ) ) ( 𝑀 ‘ 𝑢 ) = 𝑇 ) |
202 |
194 201
|
r19.29a |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) ∧ ¬ 𝑔 ∈ 𝐴 ) → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |
203 |
18 202
|
pm2.61dan |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |
204 |
1 3 4 5 36 6 7 67 9 10 11
|
cycpmconjs |
⊢ ( 𝜑 → ∃ 𝑔 ∈ ( Base ‘ 𝑆 ) 𝑄 = ( ( 𝑔 + 𝑇 ) − 𝑔 ) ) |
205 |
203 204
|
r19.29a |
⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ) |