Metamath Proof Explorer

Theorem f1otrgds

Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)

Ref Expression
Hypotheses f1otrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
f1otrkg.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
f1otrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
f1otrkg.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
f1otrkg.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
f1otrkg.j ⊢ 𝐽 = ( Itv ‘ 𝐻 )
f1otrkg.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
f1otrkg.1 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
f1otrkg.2 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
f1otrgitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
f1otrgitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion f1otrgds ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 f1otrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 f1otrkg.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
3 f1otrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 f1otrkg.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
5 f1otrkg.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
6 f1otrkg.j ⊢ 𝐽 = ( Itv ‘ 𝐻 )
7 f1otrkg.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
8 f1otrkg.1 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
9 f1otrkg.2 ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
10 f1otrgitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 f1otrgitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12 8 ralrimivva ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
13 oveq1 ⊢ ( 𝑒 = 𝑋 → ( 𝑒 𝐸 𝑓 ) = ( 𝑋 𝐸 𝑓 ) )
14 fveq2 ⊢ ( 𝑒 = 𝑋 → ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑋 ) )
15 14 oveq1d ⊢ ( 𝑒 = 𝑋 → ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
16 13 15 eqeq12d ⊢ ( 𝑒 = 𝑋 → ( ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) ↔ ( 𝑋 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) ) )
17 oveq2 ⊢ ( 𝑓 = 𝑌 → ( 𝑋 𝐸 𝑓 ) = ( 𝑋 𝐸 𝑌 ) )
18 fveq2 ⊢ ( 𝑓 = 𝑌 → ( 𝐹 ‘ 𝑓 ) = ( 𝐹 ‘ 𝑌 ) )
19 18 oveq2d ⊢ ( 𝑓 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) )
20 17 19 eqeq12d ⊢ ( 𝑓 = 𝑌 → ( ( 𝑋 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) ↔ ( 𝑋 𝐸 𝑌 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) ) )
21 16 20 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) → ( 𝑋 𝐸 𝑌 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) ) )
22 10 11 21 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) → ( 𝑋 𝐸 𝑌 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) ) )
23 12 22 mpd ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) )