rprmirredlem

	Ref	Expression
Hypotheses	rprmirredlem.1	$⊢ B = {Base}_{R}$
	rprmirredlem.2	$⊢ U = Unit (R)$
	rprmirredlem.3	$⊢ \underset{˙}{0} = 0_{R}$
	rprmirredlem.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rprmirredlem.5	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	rprmirredlem.6	$⊢ φ \to R \in IDomn$
	rprmirredlem.7	$⊢ φ \to Q \neq \underset{˙}{0}$
	rprmirredlem.8	$⊢ φ \to X \in (B ∖ U)$
	rprmirredlem.9	$⊢ φ \to Y \in B$
	rprmirredlem.10	$⊢ φ \to Q = X \underset{˙}{\cdot} Y$
	rprmirredlem.11	$⊢ φ \to Q \underset{˙}{∥} X$
Assertion	rprmirredlem	$⊢ φ \to Y \in U$

Proof

Step	Hyp	Ref	Expression
1		rprmirredlem.1	$⊢ B = {Base}_{R}$
2		rprmirredlem.2	$⊢ U = Unit (R)$
3		rprmirredlem.3	$⊢ \underset{˙}{0} = 0_{R}$
4		rprmirredlem.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		rprmirredlem.5	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
6		rprmirredlem.6	$⊢ φ \to R \in IDomn$
7		rprmirredlem.7	$⊢ φ \to Q \neq \underset{˙}{0}$
8		rprmirredlem.8	$⊢ φ \to X \in (B ∖ U)$
9		rprmirredlem.9	$⊢ φ \to Y \in B$
10		rprmirredlem.10	$⊢ φ \to Q = X \underset{˙}{\cdot} Y$
11		rprmirredlem.11	$⊢ φ \to Q \underset{˙}{∥} X$
12	6	idomcringd	$⊢ φ \to R \in CRing$
13	12	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to R \in CRing$
14	9	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Y \in B$
15	1 5 4	dvdsr	$⊢ Q \underset{˙}{∥} X \leftrightarrow (Q \in B \land \exists t \in B t \underset{˙}{\cdot} Q = X)$
16	11 15	sylib	$⊢ φ \to (Q \in B \land \exists t \in B t \underset{˙}{\cdot} Q = X)$
17	16	simpld	$⊢ φ \to Q \in B$
18	17	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \in B$
19	7	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \neq \underset{˙}{0}$
20	18 19	eldifsnd	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \in (B ∖ \{\underset{˙}{0}\})$
21	13	crngringd	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to R \in Ring$
22		simplr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \in B$
23	1 4 21 22 14	ringcld	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \underset{˙}{\cdot} Y \in B$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	1 24	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
26	21 25	syl	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to 1_{R} \in B$
27	6	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to R \in IDomn$
28		simpr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \underset{˙}{\cdot} Q = X$
29	28	oveq1d	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to (t \underset{˙}{\cdot} Q) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Y$
30	10	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q = X \underset{˙}{\cdot} Y$
31	29 30	eqtr4d	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to (t \underset{˙}{\cdot} Q) \underset{˙}{\cdot} Y = Q$
32	1 4 13 22 14 18	cringmul32d	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to (t \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Q = (t \underset{˙}{\cdot} Q) \underset{˙}{\cdot} Y$
33	1 4 24 21 18	ringlidmd	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to 1_{R} \underset{˙}{\cdot} Q = Q$
34	31 32 33	3eqtr4d	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to (t \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Q = 1_{R} \underset{˙}{\cdot} Q$
35	1 3 4 20 23 26 27 34	idomrcan	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \underset{˙}{\cdot} Y = 1_{R}$
36	16	simprd	$⊢ φ \to \exists t \in B t \underset{˙}{\cdot} Q = X$
37	35 36	reximddv3	$⊢ φ \to \exists t \in B t \underset{˙}{\cdot} Y = 1_{R}$
38	37	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to \exists t \in B t \underset{˙}{\cdot} Y = 1_{R}$
39	1 5 4	dvdsr	$⊢ Y \underset{˙}{∥} 1_{R} \leftrightarrow (Y \in B \land \exists t \in B t \underset{˙}{\cdot} Y = 1_{R})$
40	14 38 39	sylanbrc	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Y \underset{˙}{∥} 1_{R}$
41	2 24 5	crngunit	$⊢ R \in CRing \to (Y \in U \leftrightarrow Y \underset{˙}{∥} 1_{R})$
42	41	biimpar	$⊢ (R \in CRing \land Y \underset{˙}{∥} 1_{R}) \to Y \in U$
43	13 40 42	syl2anc	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Y \in U$
44	43 36	r19.29a	$⊢ φ \to Y \in U$

Metamath Proof Explorer

Theorem rprmirredlem

Proof