Metamath Proof Explorer

Theorem clwwlknonccat

Description: The concatenation of two words representing closed walks on a vertex X represents a closed walk on vertex X . The resulting walk is a "double loop", starting at vertex X , coming back to X by the first walk, following the second walk and finally coming back to X again. (Contributed by AV, 24-Apr-2022)

Ref Expression
Assertion clwwlknonccat 
|- ( ( A e. ( X ( ClWWalksNOn ` G ) M ) /\ B e. ( X ( ClWWalksNOn ` G ) N ) ) -> ( A ++ B ) e. ( X ( ClWWalksNOn ` G ) ( M + N ) ) )

Proof

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 ) ) )