Theorem resisoeq45d

Description: Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025)

	Ref	Expression
Hypotheses	resisoeq45.4	⊢ ( 𝜑 → 𝐴 = 𝐶 )
	resisoeq45.5	⊢ ( 𝜑 → 𝐵 = 𝐷 )
Assertion	resisoeq45d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐹 ↾ 𝐶 ) Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resisoeq45.4	⊢ ( 𝜑 → 𝐴 = 𝐶 )
2		resisoeq45.5	⊢ ( 𝜑 → 𝐵 = 𝐷 )
3	1	reseq2d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝐹 ↾ 𝐶 ) )
4	3 1 2	isoeq145d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐹 ↾ 𝐶 ) Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )