Theorem dvrcan5

Description: Cancellation law for common factor in ratio. ( divcan5 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016)

	Ref	Expression
Hypotheses	dvrcan5.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvrcan5.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	dvrcan5.d	⊢ / = ( /r ‘ 𝑅 )
	dvrcan5.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	dvrcan5	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 / 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dvrcan5.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvrcan5.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		dvrcan5.d	⊢ / = ( /r ‘ 𝑅 )
4		dvrcan5.t	⊢ · = ( .r ‘ 𝑅 )
5	1 2	unitss	⊢ 𝑈 ⊆ 𝐵
6		simpr3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝑈 )
7	5 6	sselid	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝐵 )
8	2 4	unitmulcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑌 · 𝑍 ) ∈ 𝑈 )
9	8	3adant3r1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑌 · 𝑍 ) ∈ 𝑈 )
10		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
11	1 4 2 10 3	dvrval	⊢ ( ( 𝑍 ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝑈 ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
12	7 9 11	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
13		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
14		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
15	2 14	unitgrp	⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
16	13 15	syl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
17		simpr2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
18	2 14	unitgrpbas	⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
19	2	fvexi	⊢ 𝑈 ∈ V
20		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
21	20 4	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
22	14 21	ressplusg	⊢ ( 𝑈 ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
23	19 22	ax-mp	⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
24	2 14 10	invrfval	⊢ ( invr ‘ 𝑅 ) = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
25	18 23 24	grpinvadd	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
26	25	oveq2d	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
27	16 17 6 26	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
28		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29	2 10 4 28	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
30	29	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
31	30	3ad2antr3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
32	2 10	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
33	32	3ad2antr3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
34	5 33	sselid	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
35	2 10	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
36	35	3ad2antr2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
37	5 36	sselid	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
38	1 4	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑍 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
39	13 7 34 37 38	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
40	1 4 28	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
41	13 37 40	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
42	31 39 41	3eqtr3d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
43	12 27 42	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
44	43	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
45		simpr1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
46	1 2 3 4	dvrass	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) )
47	13 45 7 9 46	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) )
48	1 4 2 10 3	dvrval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
49	45 17 48	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
50	44 47 49	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 / 𝑌 ) )