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	13	crngringd	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to R \in Ring$
16		simplr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \in B$
17	1 4 15 16 14	ringcld	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \underset{˙}{\cdot} Y \in B$
18		eqid	$⊢ 1_{R} = 1_{R}$
19	1 18	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
20	15 19	syl	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to 1_{R} \in B$
21	1 5 4	dvdsr	$⊢ Q \underset{˙}{∥} X \leftrightarrow (Q \in B \land \exists t \in B t \underset{˙}{\cdot} Q = X)$
22	11 21	sylib	$⊢ φ \to (Q \in B \land \exists t \in B t \underset{˙}{\cdot} Q = X)$
23	22	simpld	$⊢ φ \to Q \in B$
24	23	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \in B$
25	7	ad2antrr	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \neq \underset{˙}{0}$
26	24 25	eldifsnd	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to Q \in (B ∖ \{\underset{˙}{0}\})$
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 16 14 24	crng32d	$⊢ ((φ \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 18 15 24	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 17 20 26 27 34	idomrcan	$⊢ ((φ \land t \in B) \land t \underset{˙}{\cdot} Q = X) \to t \underset{˙}{\cdot} Y = 1_{R}$
36	22	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 18 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