Metamath Proof Explorer

Theorem wksonproplem

Description: Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop . (Contributed by AV, 16-Jan-2021)

Ref Expression
Hypotheses wksonproplem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wksonproplem.b ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
wksonproplem.d ⊢ 𝑊 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( 𝑂 ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( 𝑄 ‘ 𝑔 ) 𝑝 ) } ) )
wksonproplem.w ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑓 ( 𝑄 ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
Assertion wksonproplem ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 wksonproplem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wksonproplem.b ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
3 wksonproplem.d ⊢ 𝑊 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( 𝑂 ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( 𝑄 ‘ 𝑔 ) 𝑝 ) } ) )
4 wksonproplem.w ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑓 ( 𝑄 ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
5 1 fvexi ⊢ 𝑉 ∈ V
6 simp1 ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
7 simp2 ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
8 7 1 eleqtrdi ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
9 simp3 ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
10 9 1 eleqtrdi ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
11 wksv ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V
12 11 a1i ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V )
13 6 8 10 12 4 3 mptmpoopabovd ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( 𝑄 ‘ 𝐺 ) 𝑝 ) } )
14 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
15 14 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
16 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝑂 ‘ 𝑔 ) = ( 𝑂 ‘ 𝐺 ) )
17 16 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( 𝑂 ‘ 𝑔 ) 𝑏 ) = ( 𝑎 ( 𝑂 ‘ 𝐺 ) 𝑏 ) )
18 17 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝑎 ( 𝑂 ‘ 𝑔 ) 𝑏 ) 𝑝 ↔ 𝑓 ( 𝑎 ( 𝑂 ‘ 𝐺 ) 𝑏 ) 𝑝 ) )
19 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝑄 ‘ 𝑔 ) = ( 𝑄 ‘ 𝐺 ) )
20 19 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( 𝑄 ‘ 𝑔 ) 𝑝 ↔ 𝑓 ( 𝑄 ‘ 𝐺 ) 𝑝 ) )
21 18 20 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 ( 𝑎 ( 𝑂 ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( 𝑄 ‘ 𝑔 ) 𝑝 ) ↔ ( 𝑓 ( 𝑎 ( 𝑂 ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ 𝑓 ( 𝑄 ‘ 𝐺 ) 𝑝 ) ) )
22 3 13 15 15 21 bropfvvvv ⊢ ( ( 𝑉 ∈ V ∧ 𝑉 ∈ V ) → ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
23 5 5 22 mp2an ⊢ ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
24 3anass ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ↔ ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
25 24 anbi1i ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
26 df-3an ⊢ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
27 25 26 bitr4i ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
28 23 27 sylibr ⊢ ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
29 2 biimpd ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
30 29 imdistani ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 ) → ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
31 28 30 mpancom ⊢ ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
32 df-3an ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) ↔ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )
33 31 32 sylibr ⊢ ( 𝐹 ( 𝐴 ( 𝑊 ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( 𝑂 ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( 𝑄 ‘ 𝐺 ) 𝑃 ) ) )