Metamath Proof Explorer

Theorem seglecgr12

Description: Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion seglecgr12 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\to \left(⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩↔⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\right)$

Proof

Step Hyp Ref Expression
1 df-3an ${⊢}\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\wedge ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)↔\left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\wedge ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)$
2 seglecgr12im ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\wedge ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)\to ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)$
3 1 2 syl5bir ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\wedge ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)\to ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)$
4 3 expd ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\to \left(⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\to ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\right)$
5 simp11 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
6 simp12 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
7 simp13 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
8 simp23 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
9 simp31 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {F}\in 𝔼\left({N}\right)$
10 cgrcom ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩↔⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\right)$
11 5 6 7 8 9 10 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩↔⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\right)$
12 simp21 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
13 simp22 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
14 simp32 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {G}\in 𝔼\left({N}\right)$
15 simp33 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to {H}\in 𝔼\left({N}\right)$
16 cgrcom ${⊢}\left({N}\in ℕ\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩↔⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)$
17 5 12 13 14 15 16 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩↔⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)$
18 11 17 anbi12d ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)↔\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)$
19 df-3an ${⊢}\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\wedge ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)↔\left(\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)$
20 seglecgr12im ${⊢}\left(\left({N}\in ℕ\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\wedge \left({G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\wedge ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\to ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)$
21 5 8 9 14 15 6 7 12 13 20 syl333anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\wedge ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\to ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)$
22 19 21 syl5bir ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge ⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\to ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)$
23 22 expd ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{E},{F}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{G},{H}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to \left(⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\to ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)\right)$
24 18 23 sylbid ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\to \left(⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\to ⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩\right)\right)$
25 4 24 impbidd ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\wedge \left({F}\in 𝔼\left({N}\right)\wedge {G}\in 𝔼\left({N}\right)\wedge {H}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{C},{D}⟩\mathrm{Cgr}⟨{G},{H}⟩\right)\to \left(⟨{A},{B}⟩{\mathrm{Seg}}_{\le }⟨{C},{D}⟩↔⟨{E},{F}⟩{\mathrm{Seg}}_{\le }⟨{G},{H}⟩\right)\right)$