Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) -> A e. ( M ClWWalksN G ) ) |
2 |
1
|
adantr |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> A e. ( M ClWWalksN G ) ) |
3 |
|
simpl |
|- ( ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) -> B e. ( N ClWWalksN G ) ) |
4 |
3
|
adantl |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> B e. ( N ClWWalksN G ) ) |
5 |
|
simpr |
|- ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) -> ( A ` 0 ) = X ) |
6 |
5
|
adantr |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( A ` 0 ) = X ) |
7 |
|
simpr |
|- ( ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) -> ( B ` 0 ) = X ) |
8 |
7
|
eqcomd |
|- ( ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) -> X = ( B ` 0 ) ) |
9 |
8
|
adantl |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> X = ( B ` 0 ) ) |
10 |
6 9
|
eqtrd |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( A ` 0 ) = ( B ` 0 ) ) |
11 |
|
clwwlknccat |
|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) ) |
12 |
2 4 10 11
|
syl3anc |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) ) |
13 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
14 |
13
|
clwwlknwrd |
|- ( A e. ( M ClWWalksN G ) -> A e. Word ( Vtx ` G ) ) |
15 |
14
|
adantr |
|- ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) -> A e. Word ( Vtx ` G ) ) |
16 |
15
|
adantr |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> A e. Word ( Vtx ` G ) ) |
17 |
13
|
clwwlknwrd |
|- ( B e. ( N ClWWalksN G ) -> B e. Word ( Vtx ` G ) ) |
18 |
17
|
adantr |
|- ( ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) -> B e. Word ( Vtx ` G ) ) |
19 |
18
|
adantl |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> B e. Word ( Vtx ` G ) ) |
20 |
|
clwwlknnn |
|- ( A e. ( M ClWWalksN G ) -> M e. NN ) |
21 |
|
clwwlknlen |
|- ( A e. ( M ClWWalksN G ) -> ( # ` A ) = M ) |
22 |
|
nngt0 |
|- ( M e. NN -> 0 < M ) |
23 |
|
breq2 |
|- ( ( # ` A ) = M -> ( 0 < ( # ` A ) <-> 0 < M ) ) |
24 |
22 23
|
syl5ibrcom |
|- ( M e. NN -> ( ( # ` A ) = M -> 0 < ( # ` A ) ) ) |
25 |
20 21 24
|
sylc |
|- ( A e. ( M ClWWalksN G ) -> 0 < ( # ` A ) ) |
26 |
25
|
adantr |
|- ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) -> 0 < ( # ` A ) ) |
27 |
26
|
adantr |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> 0 < ( # ` A ) ) |
28 |
|
ccatfv0 |
|- ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ 0 < ( # ` A ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) ) |
29 |
16 19 27 28
|
syl3anc |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) ) |
30 |
29 6
|
eqtrd |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( ( A ++ B ) ` 0 ) = X ) |
31 |
12 30
|
jca |
|- ( ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) -> ( ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) /\ ( ( A ++ B ) ` 0 ) = X ) ) |
32 |
|
isclwwlknon |
|- ( A e. ( X ( ClWWalksNOn ` G ) M ) <-> ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) ) |
33 |
|
isclwwlknon |
|- ( B e. ( X ( ClWWalksNOn ` G ) N ) <-> ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) |
34 |
32 33
|
anbi12i |
|- ( ( A e. ( X ( ClWWalksNOn ` G ) M ) /\ B e. ( X ( ClWWalksNOn ` G ) N ) ) <-> ( ( A e. ( M ClWWalksN G ) /\ ( A ` 0 ) = X ) /\ ( B e. ( N ClWWalksN G ) /\ ( B ` 0 ) = X ) ) ) |
35 |
|
isclwwlknon |
|- ( ( A ++ B ) e. ( X ( ClWWalksNOn ` G ) ( M + N ) ) <-> ( ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) /\ ( ( A ++ B ) ` 0 ) = X ) ) |
36 |
31 34 35
|
3imtr4i |
|- ( ( A e. ( X ( ClWWalksNOn ` G ) M ) /\ B e. ( X ( ClWWalksNOn ` G ) N ) ) -> ( A ++ B ) e. ( X ( ClWWalksNOn ` G ) ( M + N ) ) ) |