This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024)

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