Theorem isoeq145d

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

	Ref	Expression
Hypotheses	isoeq145.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
	isoeq145.4	⊢ ( 𝜑 → 𝐴 = 𝐶 )
	isoeq145.5	⊢ ( 𝜑 → 𝐵 = 𝐷 )
Assertion	isoeq145d	⊢ ( 𝜑 → ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isoeq145.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2		isoeq145.4	⊢ ( 𝜑 → 𝐴 = 𝐶 )
3		isoeq145.5	⊢ ( 𝜑 → 𝐵 = 𝐷 )
4		isoeq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
6		isoeq4	⊢ ( 𝐴 = 𝐶 → ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐵 ) ) )
7	2 6	syl	⊢ ( 𝜑 → ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐵 ) ) )
8		isoeq5	⊢ ( 𝐵 = 𝐷 → ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )
9	3 8	syl	⊢ ( 𝜑 → ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )
10	5 7 9	3bitrd	⊢ ( 𝜑 → ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) )