ghomdiv

Description: Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	ghomdiv.1	$⊢ X = ran G$
	ghomdiv.2	$⊢ D = /_{g} (G)$
	ghomdiv.3	$⊢ C = /_{g} (H)$
Assertion	ghomdiv	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A D B) = F (A) C F (B)$

Proof

Step	Hyp	Ref	Expression
1		ghomdiv.1	$⊢ X = ran G$
2		ghomdiv.2	$⊢ D = /_{g} (G)$
3		ghomdiv.3	$⊢ C = /_{g} (H)$
4		simpl2	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to H \in GrpOp$
5		eqid	$⊢ ran H = ran H$
6	1 5	ghomf	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F : X ⟶ ran H$
7	6	ffvelrnda	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land A \in X) \to F (A) \in ran H$
8	7	adantrr	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A) \in ran H$
9	6	ffvelrnda	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land B \in X) \to F (B) \in ran H$
10	9	adantrl	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (B) \in ran H$
11	5 3	grponpcan	$⊢ (H \in GrpOp \land F (A) \in ran H \land F (B) \in ran H) \to (F (A) C F (B)) H F (B) = F (A)$
12	4 8 10 11	syl3anc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to (F (A) C F (B)) H F (B) = F (A)$
13	1 2	grponpcan	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A D B) G B = A$
14	13	3expb	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to (A D B) G B = A$
15	14	3ad2antl1	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to (A D B) G B = A$
16	15	fveq2d	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F ((A D B) G B) = F (A)$
17	1 2	grpodivcl	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B \in X$
18	17	3expb	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to A D B \in X$
19		simprr	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to B \in X$
20	18 19	jca	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to (A D B \in X \land B \in X)$
21	20	3ad2antl1	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to (A D B \in X \land B \in X)$
22	1	ghomlinOLD	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A D B \in X \land B \in X)) \to F (A D B) H F (B) = F ((A D B) G B)$
23	22	eqcomd	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A D B \in X \land B \in X)) \to F ((A D B) G B) = F (A D B) H F (B)$
24	21 23	syldan	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F ((A D B) G B) = F (A D B) H F (B)$
25	12 16 24	3eqtr2rd	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A D B) H F (B) = (F (A) C F (B)) H F (B)$
26	18	3ad2antl1	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to A D B \in X$
27	6	ffvelrnda	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land A D B \in X) \to F (A D B) \in ran H$
28	26 27	syldan	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A D B) \in ran H$
29	5 3	grpodivcl	$⊢ (H \in GrpOp \land F (A) \in ran H \land F (B) \in ran H) \to F (A) C F (B) \in ran H$
30	4 8 10 29	syl3anc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A) C F (B) \in ran H$
31	5	grporcan	$⊢ (H \in GrpOp \land (F (A D B) \in ran H \land F (A) C F (B) \in ran H \land F (B) \in ran H)) \to (F (A D B) H F (B) = (F (A) C F (B)) H F (B) \leftrightarrow F (A D B) = F (A) C F (B))$
32	4 28 30 10 31	syl13anc	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to (F (A D B) H F (B) = (F (A) C F (B)) H F (B) \leftrightarrow F (A D B) = F (A) C F (B))$
33	25 32	mpbid	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A D B) = F (A) C F (B)$

Metamath Proof Explorer

Theorem ghomdiv

Proof