rngosubdi

Description: Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	ringsubdi.1	$⊢ G = 1^{st} (R)$
	ringsubdi.2	$⊢ H = 2^{nd} (R)$
	ringsubdi.3	$⊢ X = ran G$
	ringsubdi.4	$⊢ D = /_{g} (G)$
Assertion	rngosubdi	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B D C) = (A H B) D (A H C)$

Proof

Step	Hyp	Ref	Expression
1		ringsubdi.1	$⊢ G = 1^{st} (R)$
2		ringsubdi.2	$⊢ H = 2^{nd} (R)$
3		ringsubdi.3	$⊢ X = ran G$
4		ringsubdi.4	$⊢ D = /_{g} (G)$
5		eqid	$⊢ inv (G) = inv (G)$
6	1 3 5 4	rngosub	$⊢ (R \in RingOps \land B \in X \land C \in X) \to B D C = B G inv (G) (C)$
7	6	3adant3r1	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to B D C = B G inv (G) (C)$
8	7	oveq2d	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B D C) = A H (B G inv (G) (C))$
9	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A H B \in X$
10	9	3adant3r3	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H B \in X$
11	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land C \in X) \to A H C \in X$
12	11	3adant3r2	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H C \in X$
13	10 12	jca	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B \in X \land A H C \in X)$
14	1 3 5 4	rngosub	$⊢ (R \in RingOps \land A H B \in X \land A H C \in X) \to (A H B) D (A H C) = (A H B) G inv (G) (A H C)$
15	14	3expb	$⊢ (R \in RingOps \land (A H B \in X \land A H C \in X)) \to (A H B) D (A H C) = (A H B) G inv (G) (A H C)$
16	13 15	syldan	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) D (A H C) = (A H B) G inv (G) (A H C)$
17		idd	$⊢ R \in RingOps \to (A \in X \to A \in X)$
18		idd	$⊢ R \in RingOps \to (B \in X \to B \in X)$
19	1 3 5	rngonegcl	$⊢ (R \in RingOps \land C \in X) \to inv (G) (C) \in X$
20	19	ex	$⊢ R \in RingOps \to (C \in X \to inv (G) (C) \in X)$
21	17 18 20	3anim123d	$⊢ R \in RingOps \to ((A \in X \land B \in X \land C \in X) \to (A \in X \land B \in X \land inv (G) (C) \in X))$
22	21	imp	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A \in X \land B \in X \land inv (G) (C) \in X)$
23	1 2 3	rngodi	$⊢ (R \in RingOps \land (A \in X \land B \in X \land inv (G) (C) \in X)) \to A H (B G inv (G) (C)) = (A H B) G (A H inv (G) (C))$
24	22 23	syldan	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B G inv (G) (C)) = (A H B) G (A H inv (G) (C))$
25	1 2 3 5	rngonegrmul	$⊢ (R \in RingOps \land A \in X \land C \in X) \to inv (G) (A H C) = A H inv (G) (C)$
26	25	3adant3r2	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to inv (G) (A H C) = A H inv (G) (C)$
27	26	oveq2d	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) G inv (G) (A H C) = (A H B) G (A H inv (G) (C))$
28	24 27	eqtr4d	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B G inv (G) (C)) = (A H B) G inv (G) (A H C)$
29	16 28	eqtr4d	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) D (A H C) = A H (B G inv (G) (C))$
30	8 29	eqtr4d	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B D C) = (A H B) D (A H C)$

Metamath Proof Explorer

Theorem rngosubdi

Proof