Metamath Proof Explorer

Theorem clwwlknon2num

Description: In a K-regular graph G , there are K closed walks on vertex X of length 2 . (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 25-Mar-2022)

Ref Expression
Assertion clwwlknon2num 
|- ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ClWWalksNOn ` G ) = ( ClWWalksNOn ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 2 3 clwwlknon2x 
 |-  ( X ( ClWWalksNOn ` G ) 2 ) = { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) }
5 4 a1i 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( X ( ClWWalksNOn ` G ) 2 ) = { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) } )
6 5 fveq2d 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = ( # ` { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) } ) )
7 3ancomb 
 |-  ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = X /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) <-> ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) )
8 7 rabbii 
 |-  { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ ( w ` 0 ) = X /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } = { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) }
9 8 fveq2i 
 |-  ( # ` { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ ( w ` 0 ) = X /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = ( # ` { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) } )
10 2 rusgrnumwrdl2 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ ( w ` 0 ) = X /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) } ) = K )
11 9 10 eqtr3id 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` { w e. Word ( Vtx ` G ) | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) /\ ( w ` 0 ) = X ) } ) = K )
12 6 11 eqtrd 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )