subrgdv

Description: A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrgdv.1	$⊢ S = R ↾_{𝑠} A$
	subrgdv.2	$⊢ \underset{˙}{\times} = /_{r} (R)$
	subrgdv.3	$⊢ U = Unit (S)$
	subrgdv.4	$⊢ E = /_{r} (S)$
Assertion	subrgdv	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \underset{˙}{\times} Y = X E Y$

Proof

Step	Hyp	Ref	Expression
1		subrgdv.1	$⊢ S = R ↾_{𝑠} A$
2		subrgdv.2	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		subrgdv.3	$⊢ U = Unit (S)$
4		subrgdv.4	$⊢ E = /_{r} (S)$
5		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
6		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
7	1 5 3 6	subrginv	$⊢ (A \in SubRing (R) \land Y \in U) \to {inv}_{r} (R) (Y) = {inv}_{r} (S) (Y)$
8	7	3adant2	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to {inv}_{r} (R) (Y) = {inv}_{r} (S) (Y)$
9	8	oveq2d	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \cdot_{R} {inv}_{r} (R) (Y) = X \cdot_{R} {inv}_{r} (S) (Y)$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 10	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
12	11	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to \cdot_{R} = \cdot_{S}$
13	12	oveqd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \cdot_{R} {inv}_{r} (S) (Y) = X \cdot_{S} {inv}_{r} (S) (Y)$
14	9 13	eqtrd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \cdot_{R} {inv}_{r} (R) (Y) = X \cdot_{S} {inv}_{r} (S) (Y)$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	15	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
17	16	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to A \subseteq {Base}_{R}$
18		simp2	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \in A$
19	17 18	sseldd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \in {Base}_{R}$
20		eqid	$⊢ Unit (R) = Unit (R)$
21	1 20 3	subrguss	$⊢ A \in SubRing (R) \to U \subseteq Unit (R)$
22	21	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to U \subseteq Unit (R)$
23		simp3	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to Y \in U$
24	22 23	sseldd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to Y \in Unit (R)$
25	15 10 20 5 2	dvrval	$⊢ (X \in {Base}_{R} \land Y \in Unit (R)) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
26	19 24 25	syl2anc	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \underset{˙}{\times} Y = X \cdot_{R} {inv}_{r} (R) (Y)$
27	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
28	27	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to A = {Base}_{S}$
29	18 28	eleqtrd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \in {Base}_{S}$
30		eqid	$⊢ {Base}_{S} = {Base}_{S}$
31		eqid	$⊢ \cdot_{S} = \cdot_{S}$
32	30 31 3 6 4	dvrval	$⊢ (X \in {Base}_{S} \land Y \in U) \to X E Y = X \cdot_{S} {inv}_{r} (S) (Y)$
33	29 23 32	syl2anc	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X E Y = X \cdot_{S} {inv}_{r} (S) (Y)$
34	14 26 33	3eqtr4d	$⊢ (A \in SubRing (R) \land X \in A \land Y \in U) \to X \underset{˙}{\times} Y = X E Y$

Metamath Proof Explorer

Theorem subrgdv

Proof