rdivmuldivd

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017)

	Ref	Expression
Hypotheses	dvrdir.b	$⊢ B = {Base}_{R}$
	dvrdir.u	$⊢ U = Unit (R)$
	dvrdir.p	$⊢ \underset{˙}{+} = +_{R}$
	dvrdir.t	$⊢ \underset{˙}{\times} = /_{r} (R)$
	rdivmuldivd.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rdivmuldivd.r	$⊢ φ \to R \in CRing$
	rdivmuldivd.a	$⊢ φ \to X \in B$
	rdivmuldivd.b	$⊢ φ \to Y \in U$
	rdivmuldivd.c	$⊢ φ \to Z \in B$
	rdivmuldivd.d	$⊢ φ \to W \in U$
Assertion	rdivmuldivd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} W)$

Proof

Step	Hyp	Ref	Expression
1		dvrdir.b	$⊢ B = {Base}_{R}$
2		dvrdir.u	$⊢ U = Unit (R)$
3		dvrdir.p	$⊢ \underset{˙}{+} = +_{R}$
4		dvrdir.t	$⊢ \underset{˙}{\times} = /_{r} (R)$
5		rdivmuldivd.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		rdivmuldivd.r	$⊢ φ \to R \in CRing$
7		rdivmuldivd.a	$⊢ φ \to X \in B$
8		rdivmuldivd.b	$⊢ φ \to Y \in U$
9		rdivmuldivd.c	$⊢ φ \to Z \in B$
10		rdivmuldivd.d	$⊢ φ \to W \in U$
11		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
12	1 5 2 11 4	dvrval	$⊢ (X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
13	12	oveq1d	$⊢ (X \in B \land Y \in U) \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} (Z \underset{˙}{\times} W)$
14	7 8 13	syl2anc	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} (Z \underset{˙}{\times} W)$
15		crngring	$⊢ R \in CRing \to R \in Ring$
16	6 15	syl	$⊢ φ \to R \in Ring$
17	1 2	unitss	$⊢ U \subseteq B$
18	2 11	unitinvcl	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \in U$
19	16 8 18	syl2anc	$⊢ φ \to {inv}_{r} (R) (Y) \in U$
20	17 19	sseldi	$⊢ φ \to {inv}_{r} (R) (Y) \in B$
21	1 2 4	dvrcl	$⊢ (R \in Ring \land Z \in B \land W \in U) \to Z \underset{˙}{\times} W \in B$
22	16 9 10 21	syl3anc	$⊢ φ \to Z \underset{˙}{\times} W \in B$
23	1 5	ringass	$⊢ (R \in Ring \land (X \in B \land {inv}_{r} (R) (Y) \in B \land Z \underset{˙}{\times} W \in B)) \to (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W))$
24	16 7 20 22 23	syl13anc	$⊢ φ \to (X \underset{˙}{\cdot} {inv}_{r} (R) (Y)) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W))$
25	1 5	crngcom	$⊢ (R \in CRing \land {inv}_{r} (R) (Y) \in B \land Z \underset{˙}{\times} W \in B) \to {inv}_{r} (R) (Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
26	6 20 22 25	syl3anc	$⊢ φ \to {inv}_{r} (R) (Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
27	26	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} ({inv}_{r} (R) (Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W)) = X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
28	14 24 27	3eqtrd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
29		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{R} ↾_{𝑠} U$
30	2 29	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} U \in Grp$
31	16 30	syl	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} U \in Grp$
32	2 29	unitgrpbas	$⊢ U = {Base}_{({mulGrp}_{R} ↾_{𝑠} U)}$
33		eqid	$⊢ +_{({mulGrp}_{R} ↾_{𝑠} U)} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
34	2 29 11	invrfval	$⊢ {inv}_{r} (R) = {inv}_{g} ({mulGrp}_{R} ↾_{𝑠} U)$
35	32 33 34	grpinvadd	$⊢ ({mulGrp}_{R} ↾_{𝑠} U \in Grp \land Y \in U \land W \in U) \to {inv}_{r} (R) (Y +_{({mulGrp}_{R} ↾_{𝑠} U)} W) = {inv}_{r} (R) (W) +_{({mulGrp}_{R} ↾_{𝑠} U)} {inv}_{r} (R) (Y)$
36	31 8 10 35	syl3anc	$⊢ φ \to {inv}_{r} (R) (Y +_{({mulGrp}_{R} ↾_{𝑠} U)} W) = {inv}_{r} (R) (W) +_{({mulGrp}_{R} ↾_{𝑠} U)} {inv}_{r} (R) (Y)$
37		eqid	$⊢ {mulGrp}_{(R ↾_{𝑠} U)} = {mulGrp}_{(R ↾_{𝑠} U)}$
38	2	fvexi	$⊢ U \in V$
39		eqid	$⊢ R ↾_{𝑠} U = R ↾_{𝑠} U$
40	39 5	ressmulr	$⊢ U \in V \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} U)}$
41	38 40	ax-mp	$⊢ \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} U)}$
42	37 41	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{(R ↾_{𝑠} U)}}$
43		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
44	39 43	mgpress	$⊢ (R \in Ring \land U \in V) \to {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{(R ↾_{𝑠} U)}$
45	16 38 44	sylancl	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{(R ↾_{𝑠} U)}$
46	45	fveq2d	$⊢ φ \to +_{({mulGrp}_{R} ↾_{𝑠} U)} = +_{{mulGrp}_{(R ↾_{𝑠} U)}}$
47	42 46	eqtr4id	$⊢ φ \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
48	47	oveqd	$⊢ φ \to Y \underset{˙}{\cdot} W = Y +_{({mulGrp}_{R} ↾_{𝑠} U)} W$
49	48	fveq2d	$⊢ φ \to {inv}_{r} (R) (Y \underset{˙}{\cdot} W) = {inv}_{r} (R) (Y +_{({mulGrp}_{R} ↾_{𝑠} U)} W)$
50	47	oveqd	$⊢ φ \to {inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = {inv}_{r} (R) (W) +_{({mulGrp}_{R} ↾_{𝑠} U)} {inv}_{r} (R) (Y)$
51	36 49 50	3eqtr4d	$⊢ φ \to {inv}_{r} (R) (Y \underset{˙}{\cdot} W) = {inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
52	51	oveq2d	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} W) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} ({inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
53	1 5	ringcl	$⊢ (R \in Ring \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
54	16 7 9 53	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
55	2 5	unitmulcl	$⊢ (R \in Ring \land Y \in U \land W \in U) \to Y \underset{˙}{\cdot} W \in U$
56	16 8 10 55	syl3anc	$⊢ φ \to Y \underset{˙}{\cdot} W \in U$
57	1 5 2 11 4	dvrval	$⊢ (X \underset{˙}{\cdot} Z \in B \land Y \underset{˙}{\cdot} W \in U) \to (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} W) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} W)$
58	54 56 57	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} W) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} W)$
59	2 11	unitinvcl	$⊢ (R \in Ring \land W \in U) \to {inv}_{r} (R) (W) \in U$
60	16 10 59	syl2anc	$⊢ φ \to {inv}_{r} (R) (W) \in U$
61	17 60	sseldi	$⊢ φ \to {inv}_{r} (R) (W) \in B$
62	1 5	ringass	$⊢ (R \in Ring \land (X \in B \land Z \in B \land {inv}_{r} (R) (W) \in B)) \to (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W) = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} {inv}_{r} (R) (W))$
63	16 7 9 61 62	syl13anc	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W) = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} {inv}_{r} (R) (W))$
64	1 5 2 11 4	dvrval	$⊢ (Z \in B \land W \in U) \to Z \underset{˙}{\times} W = Z \underset{˙}{\cdot} {inv}_{r} (R) (W)$
65	9 10 64	syl2anc	$⊢ φ \to Z \underset{˙}{\times} W = Z \underset{˙}{\cdot} {inv}_{r} (R) (W)$
66	65	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} {inv}_{r} (R) (W))$
67	63 66	eqtr4d	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W) = X \underset{˙}{\cdot} (Z \underset{˙}{\times} W)$
68	67	oveq1d	$⊢ φ \to ((X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = (X \underset{˙}{\cdot} (Z \underset{˙}{\times} W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
69	1 5	ringass	$⊢ (R \in Ring \land (X \underset{˙}{\cdot} Z \in B \land {inv}_{r} (R) (W) \in B \land {inv}_{r} (R) (Y) \in B)) \to ((X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} ({inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
70	16 54 61 20 69	syl13anc	$⊢ φ \to ((X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} {inv}_{r} (R) (W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} ({inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
71	1 5	ringass	$⊢ (R \in Ring \land (X \in B \land Z \underset{˙}{\times} W \in B \land {inv}_{r} (R) (Y) \in B)) \to (X \underset{˙}{\cdot} (Z \underset{˙}{\times} W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
72	16 7 22 20 71	syl13anc	$⊢ φ \to (X \underset{˙}{\cdot} (Z \underset{˙}{\times} W)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
73	68 70 72	3eqtr3rd	$⊢ φ \to X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y)) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} ({inv}_{r} (R) (W) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
74	52 58 73	3eqtr4rd	$⊢ φ \to X \underset{˙}{\cdot} ((Z \underset{˙}{\times} W) \underset{˙}{\cdot} {inv}_{r} (R) (Y)) = (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} W)$
75	28 74	eqtrd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} (Z \underset{˙}{\times} W) = (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} W)$

Metamath Proof Explorer

Theorem rdivmuldivd

Proof