brecop2

Description: Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996) (Revised by AV, 12-Jul-2022)

	Ref	Expression
Hypotheses	brecop2.1	$⊢ dom \underset{˙}{\sim} = G \times G$
	brecop2.2	$⊢ H = (G \times G) / \underset{˙}{\sim}$
	brecop2.3	$⊢ R \subseteq H \times H$
	brecop2.4	$⊢ \underset{˙}{\leq} \subseteq G \times G$
	brecop2.5	$⊢ \neg \emptyset \in G$
	brecop2.6	$⊢ dom \underset{˙}{+} = G \times G$
	brecop2.7	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ([⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C))$
Assertion	brecop2	$⊢ [⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C)$

Proof

Step	Hyp	Ref	Expression
1		brecop2.1	$⊢ dom \underset{˙}{\sim} = G \times G$
2		brecop2.2	$⊢ H = (G \times G) / \underset{˙}{\sim}$
3		brecop2.3	$⊢ R \subseteq H \times H$
4		brecop2.4	$⊢ \underset{˙}{\leq} \subseteq G \times G$
5		brecop2.5	$⊢ \neg \emptyset \in G$
6		brecop2.6	$⊢ dom \underset{˙}{+} = G \times G$
7		brecop2.7	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ([⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C))$
8	3	brel	$⊢ [⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \to ([⟨A, B⟩] \underset{˙}{\sim} \in H \land [⟨C, D⟩] \underset{˙}{\sim} \in H)$
9		ecelqsdm	$⊢ (dom \underset{˙}{\sim} = G \times G \land [⟨A, B⟩] \underset{˙}{\sim} \in ((G \times G) / \underset{˙}{\sim})) \to ⟨A, B⟩ \in (G \times G)$
10	1 9	mpan	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \in ((G \times G) / \underset{˙}{\sim}) \to ⟨A, B⟩ \in (G \times G)$
11	10 2	eleq2s	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \in H \to ⟨A, B⟩ \in (G \times G)$
12		opelxp	$⊢ ⟨A, B⟩ \in (G \times G) \leftrightarrow (A \in G \land B \in G)$
13	11 12	sylib	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \in H \to (A \in G \land B \in G)$
14		ecelqsdm	$⊢ (dom \underset{˙}{\sim} = G \times G \land [⟨C, D⟩] \underset{˙}{\sim} \in ((G \times G) / \underset{˙}{\sim})) \to ⟨C, D⟩ \in (G \times G)$
15	1 14	mpan	$⊢ [⟨C, D⟩] \underset{˙}{\sim} \in ((G \times G) / \underset{˙}{\sim}) \to ⟨C, D⟩ \in (G \times G)$
16	15 2	eleq2s	$⊢ [⟨C, D⟩] \underset{˙}{\sim} \in H \to ⟨C, D⟩ \in (G \times G)$
17		opelxp	$⊢ ⟨C, D⟩ \in (G \times G) \leftrightarrow (C \in G \land D \in G)$
18	16 17	sylib	$⊢ [⟨C, D⟩] \underset{˙}{\sim} \in H \to (C \in G \land D \in G)$
19	13 18	anim12i	$⊢ ([⟨A, B⟩] \underset{˙}{\sim} \in H \land [⟨C, D⟩] \underset{˙}{\sim} \in H) \to ((A \in G \land B \in G) \land (C \in G \land D \in G))$
20	8 19	syl	$⊢ [⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \to ((A \in G \land B \in G) \land (C \in G \land D \in G))$
21	4	brel	$⊢ (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C) \to (A \underset{˙}{+} D \in G \land B \underset{˙}{+} C \in G)$
22	6 5	ndmovrcl	$⊢ A \underset{˙}{+} D \in G \to (A \in G \land D \in G)$
23	6 5	ndmovrcl	$⊢ B \underset{˙}{+} C \in G \to (B \in G \land C \in G)$
24	22 23	anim12i	$⊢ (A \underset{˙}{+} D \in G \land B \underset{˙}{+} C \in G) \to ((A \in G \land D \in G) \land (B \in G \land C \in G))$
25	21 24	syl	$⊢ (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C) \to ((A \in G \land D \in G) \land (B \in G \land C \in G))$
26		an42	$⊢ ((A \in G \land D \in G) \land (B \in G \land C \in G)) \leftrightarrow ((A \in G \land B \in G) \land (C \in G \land D \in G))$
27	25 26	sylib	$⊢ (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C) \to ((A \in G \land B \in G) \land (C \in G \land D \in G))$
28	20 27 7	pm5.21nii	$⊢ [⟨A, B⟩] \underset{˙}{\sim} R [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow (A \underset{˙}{+} D) \underset{˙}{\leq} (B \underset{˙}{+} C)$

Metamath Proof Explorer

Theorem brecop2

Proof