lringuplu

Description: If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025) (Revised by SN, 23-Feb-2025)

	Ref	Expression
Hypotheses	lring.b	$⊢ φ \to B = {Base}_{R}$
	lring.u	$⊢ φ \to U = Unit (R)$
	lring.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	lring.l	No typesetting found for \|- ( ph -> R e. LRing ) with typecode \|-
	lring.s	$⊢ φ \to X \underset{˙}{+} Y \in U$
	lring.x	$⊢ φ \to X \in B$
	lring.y	$⊢ φ \to Y \in B$
Assertion	lringuplu	$⊢ φ \to (X \in U \lor Y \in U)$

Proof

Step	Hyp	Ref	Expression
1		lring.b	$⊢ φ \to B = {Base}_{R}$
2		lring.u	$⊢ φ \to U = Unit (R)$
3		lring.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
4		lring.l	Could not format ( ph -> R e. LRing ) : No typesetting found for \|- ( ph -> R e. LRing ) with typecode \|-
5		lring.s	$⊢ φ \to X \underset{˙}{+} Y \in U$
6		lring.x	$⊢ φ \to X \in B$
7		lring.y	$⊢ φ \to Y \in B$
8		lringring	Could not format ( R e. LRing -> R e. Ring ) : No typesetting found for \|- ( R e. LRing -> R e. Ring ) with typecode \|-
9	4 8	syl	$⊢ φ \to R \in Ring$
10	6 1	eleqtrd	$⊢ φ \to X \in {Base}_{R}$
11	5 2	eleqtrd	$⊢ φ \to X \underset{˙}{+} Y \in Unit (R)$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ Unit (R) = Unit (R)$
14		eqid	$⊢ /_{r} (R) = /_{r} (R)$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	12 13 14 15	dvrcan1	$⊢ (R \in Ring \land X \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R)) \to (X /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = X$
17	9 10 11 16	syl3anc	$⊢ φ \to (X /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = X$
18	17	adantr	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (X /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = X$
19	9	adantr	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to R \in Ring$
20		simpr	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)$
21	11	adantr	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to X \underset{˙}{+} Y \in Unit (R)$
22	13 15	unitmulcl	$⊢ (R \in Ring \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \land X \underset{˙}{+} Y \in Unit (R)) \to (X /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) \in Unit (R)$
23	19 20 21 22	syl3anc	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (X /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) \in Unit (R)$
24	18 23	eqeltrrd	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to X \in Unit (R)$
25	2	adantr	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to U = Unit (R)$
26	24 25	eleqtrrd	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to X \in U$
27	26	orcd	$⊢ (φ \land X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (X \in U \lor Y \in U)$
28	7 1	eleqtrd	$⊢ φ \to Y \in {Base}_{R}$
29	12 13 14 15	dvrcan1	$⊢ (R \in Ring \land Y \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R)) \to (Y /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = Y$
30	9 28 11 29	syl3anc	$⊢ φ \to (Y /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = Y$
31	30	adantr	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (Y /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) = Y$
32	9	adantr	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to R \in Ring$
33		simpr	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)$
34	11	adantr	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to X \underset{˙}{+} Y \in Unit (R)$
35	13 15	unitmulcl	$⊢ (R \in Ring \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \land X \underset{˙}{+} Y \in Unit (R)) \to (Y /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) \in Unit (R)$
36	32 33 34 35	syl3anc	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (Y /_{r} (R) (X \underset{˙}{+} Y)) \cdot_{R} (X \underset{˙}{+} Y) \in Unit (R)$
37	31 36	eqeltrrd	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to Y \in Unit (R)$
38	2	adantr	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to U = Unit (R)$
39	37 38	eleqtrrd	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to Y \in U$
40	39	olcd	$⊢ (φ \land Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)) \to (X \in U \lor Y \in U)$
41		eqid	$⊢ +_{R} = +_{R}$
42	12 13 41 14	dvrdir	$⊢ (R \in Ring \land (X \in {Base}_{R} \land Y \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R))) \to (X +_{R} Y) /_{r} (R) (X \underset{˙}{+} Y) = (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y))$
43	9 10 28 11 42	syl13anc	$⊢ φ \to (X +_{R} Y) /_{r} (R) (X \underset{˙}{+} Y) = (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y))$
44	3	eqcomd	$⊢ φ \to +_{R} = \underset{˙}{+}$
45	44	oveqd	$⊢ φ \to X +_{R} Y = X \underset{˙}{+} Y$
46	9	ringgrpd	$⊢ φ \to R \in Grp$
47	12 41 46 10 28	grpcld	$⊢ φ \to X +_{R} Y \in {Base}_{R}$
48		eqid	$⊢ 1_{R} = 1_{R}$
49	12 13 14 48	dvreq1	$⊢ (R \in Ring \land X +_{R} Y \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R)) \to ((X +_{R} Y) /_{r} (R) (X \underset{˙}{+} Y) = 1_{R} \leftrightarrow X +_{R} Y = X \underset{˙}{+} Y)$
50	9 47 11 49	syl3anc	$⊢ φ \to ((X +_{R} Y) /_{r} (R) (X \underset{˙}{+} Y) = 1_{R} \leftrightarrow X +_{R} Y = X \underset{˙}{+} Y)$
51	45 50	mpbird	$⊢ φ \to (X +_{R} Y) /_{r} (R) (X \underset{˙}{+} Y) = 1_{R}$
52	43 51	eqtr3d	$⊢ φ \to (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y)) = 1_{R}$
53		oveq2	$⊢ v = Y /_{r} (R) (X \underset{˙}{+} Y) \to (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y))$
54	53	eqeq1d	$⊢ v = Y /_{r} (R) (X \underset{˙}{+} Y) \to ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R} \leftrightarrow (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y)) = 1_{R})$
55		eleq1	$⊢ v = Y /_{r} (R) (X \underset{˙}{+} Y) \to (v \in Unit (R) \leftrightarrow Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R))$
56	55	orbi2d	$⊢ v = Y /_{r} (R) (X \underset{˙}{+} Y) \to ((X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R)) \leftrightarrow (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)))$
57	54 56	imbi12d	$⊢ v = Y /_{r} (R) (X \underset{˙}{+} Y) \to (((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R))) \leftrightarrow ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y)) = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R))))$
58		oveq1	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to u +_{R} v = (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v$
59	58	eqeq1d	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to (u +_{R} v = 1_{R} \leftrightarrow (X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R})$
60		eleq1	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to (u \in Unit (R) \leftrightarrow X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R))$
61	60	orbi1d	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to ((u \in Unit (R) \lor v \in Unit (R)) \leftrightarrow (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R)))$
62	59 61	imbi12d	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to ((u +_{R} v = 1_{R} \to (u \in Unit (R) \lor v \in Unit (R))) \leftrightarrow ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R))))$
63	62	ralbidv	$⊢ u = X /_{r} (R) (X \underset{˙}{+} Y) \to (\forall v \in {Base}_{R} (u +_{R} v = 1_{R} \to (u \in Unit (R) \lor v \in Unit (R))) \leftrightarrow \forall v \in {Base}_{R} ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R))))$
64	12 41 48 13	islring	Could not format ( R e. LRing <-> ( R e. NzRing /\ A. u e. ( Base ` R ) A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) ) : No typesetting found for \|- ( R e. LRing <-> ( R e. NzRing /\ A. u e. ( Base ` R ) A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) ) with typecode \|-
65	4 64	sylib	$⊢ φ \to (R \in NzRing \land \forall u \in {Base}_{R} \forall v \in {Base}_{R} (u +_{R} v = 1_{R} \to (u \in Unit (R) \lor v \in Unit (R))))$
66	65	simprd	$⊢ φ \to \forall u \in {Base}_{R} \forall v \in {Base}_{R} (u +_{R} v = 1_{R} \to (u \in Unit (R) \lor v \in Unit (R)))$
67	12 13 14	dvrcl	$⊢ (R \in Ring \land X \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R)) \to X /_{r} (R) (X \underset{˙}{+} Y) \in {Base}_{R}$
68	9 10 11 67	syl3anc	$⊢ φ \to X /_{r} (R) (X \underset{˙}{+} Y) \in {Base}_{R}$
69	63 66 68	rspcdva	$⊢ φ \to \forall v \in {Base}_{R} ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} v = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor v \in Unit (R)))$
70	12 13 14	dvrcl	$⊢ (R \in Ring \land Y \in {Base}_{R} \land X \underset{˙}{+} Y \in Unit (R)) \to Y /_{r} (R) (X \underset{˙}{+} Y) \in {Base}_{R}$
71	9 28 11 70	syl3anc	$⊢ φ \to Y /_{r} (R) (X \underset{˙}{+} Y) \in {Base}_{R}$
72	57 69 71	rspcdva	$⊢ φ \to ((X /_{r} (R) (X \underset{˙}{+} Y)) +_{R} (Y /_{r} (R) (X \underset{˙}{+} Y)) = 1_{R} \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R)))$
73	52 72	mpd	$⊢ φ \to (X /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R) \lor Y /_{r} (R) (X \underset{˙}{+} Y) \in Unit (R))$
74	27 40 73	mpjaodan	$⊢ φ \to (X \in U \lor Y \in U)$

Metamath Proof Explorer

Theorem lringuplu

Proof