Metamath Proof Explorer

Theorem uhgr3cyclexlem

Description: Lemma for uhgr3cyclex . (Contributed by AV, 12-Feb-2021)

Ref Expression
Hypotheses uhgr3cyclex.v ⊢ V = Vtx ⁡ G
uhgr3cyclex.e ⊢ E = Edg ⁡ G
uhgr3cyclex.i ⊢ I = iEdg ⁡ G
Assertion uhgr3cyclexlem ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ J ∈ dom ⁡ I ∧ B C = I ⁡ J ∧ K ∈ dom ⁡ I ∧ C A = I ⁡ K → J ≠ K

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v ⊢ V = Vtx ⁡ G
2 uhgr3cyclex.e ⊢ E = Edg ⁡ G
3 uhgr3cyclex.i ⊢ I = iEdg ⁡ G
4 fveq2 ⊢ J = K → I ⁡ J = I ⁡ K
5 4 eqeq2d ⊢ J = K → B C = I ⁡ J ↔ B C = I ⁡ K
6 eqeq2 ⊢ I ⁡ K = C A → B C = I ⁡ K ↔ B C = C A
7 6 eqcoms ⊢ C A = I ⁡ K → B C = I ⁡ K ↔ B C = C A
8 prcom ⊢ C A = A C
9 8 eqeq1i ⊢ C A = B C ↔ A C = B C
10 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
11 simpr ⊢ A ∈ V ∧ B ∈ V → B ∈ V
12 10 11 preq1b ⊢ A ∈ V ∧ B ∈ V → A C = B C ↔ A = B
13 12 biimpcd ⊢ A C = B C → A ∈ V ∧ B ∈ V → A = B
14 9 13 sylbi ⊢ C A = B C → A ∈ V ∧ B ∈ V → A = B
15 14 eqcoms ⊢ B C = C A → A ∈ V ∧ B ∈ V → A = B
16 7 15 syl6bi ⊢ C A = I ⁡ K → B C = I ⁡ K → A ∈ V ∧ B ∈ V → A = B
17 16 adantl ⊢ K ∈ dom ⁡ I ∧ C A = I ⁡ K → B C = I ⁡ K → A ∈ V ∧ B ∈ V → A = B
18 17 com12 ⊢ B C = I ⁡ K → K ∈ dom ⁡ I ∧ C A = I ⁡ K → A ∈ V ∧ B ∈ V → A = B
19 5 18 syl6bi ⊢ J = K → B C = I ⁡ J → K ∈ dom ⁡ I ∧ C A = I ⁡ K → A ∈ V ∧ B ∈ V → A = B
20 19 adantld ⊢ J = K → J ∈ dom ⁡ I ∧ B C = I ⁡ J → K ∈ dom ⁡ I ∧ C A = I ⁡ K → A ∈ V ∧ B ∈ V → A = B
21 20 com14 ⊢ A ∈ V ∧ B ∈ V → J ∈ dom ⁡ I ∧ B C = I ⁡ J → K ∈ dom ⁡ I ∧ C A = I ⁡ K → J = K → A = B
22 21 imp32 ⊢ A ∈ V ∧ B ∈ V ∧ J ∈ dom ⁡ I ∧ B C = I ⁡ J ∧ K ∈ dom ⁡ I ∧ C A = I ⁡ K → J = K → A = B
23 22 necon3d ⊢ A ∈ V ∧ B ∈ V ∧ J ∈ dom ⁡ I ∧ B C = I ⁡ J ∧ K ∈ dom ⁡ I ∧ C A = I ⁡ K → A ≠ B → J ≠ K
24 23 impancom ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → J ∈ dom ⁡ I ∧ B C = I ⁡ J ∧ K ∈ dom ⁡ I ∧ C A = I ⁡ K → J ≠ K
25 24 imp ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ J ∈ dom ⁡ I ∧ B C = I ⁡ J ∧ K ∈ dom ⁡ I ∧ C A = I ⁡ K → J ≠ K