Theorem dvdsruasso 33721

Description: Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.)

Hypotheses

Ref	Expression
dvdsrspss.b	⊢ 𝐵 = (Base‘𝑅)
dvdsrspss.k	⊢ 𝐾 = (RSpan‘𝑅)
dvdsrspss.d	⊢ ∥ = (∥r‘𝑅)
dvdsrspss.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
dvdsrspss.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
dvdsruassoi.1	⊢ 𝑈 = (Unit‘𝑅)
dvdsruassoi.2	⊢ · = (.r‘𝑅)
dvdsruasso.r	⊢ (𝜑 → 𝑅 ∈ IDomn)

Assertion

Ref	Expression
dvdsruasso	⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌))

Distinct variable groups:   𝑢, ·   𝑢, ∥   𝑢,𝐵   𝑢,𝑅   𝑢,𝑈   𝑢,𝑋   𝑢,𝑌   𝜑,𝑢

Allowed substitution hint:   𝐾(𝑢)

Proof of Theorem dvdsruasso

Dummy variables 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvdsrspss.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
2		dvdsrspss.d	. . . . . 6 ⊢ ∥ = (∥r‘𝑅)
3		dvdsruassoi.2	. . . . . 6 ⊢ · = (.r‘𝑅)
4	1, 2, 3	dvdsr 20469	. . . . 5 ⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌))
5		dvdsrspss.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
6	5	biantrurd 542	. . . . 5 ⊢ (𝜑 → (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌)))
7	4, 6	bitr4id 293	. . . 4 ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌))
8	1, 2, 3	dvdsr 20469	. . . . 5 ⊢ (𝑌 ∥ 𝑋 ↔ (𝑌 ∈ 𝐵 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋))
9		dvdsrspss.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
10	9	biantrurd 542	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋 ↔ (𝑌 ∈ 𝐵 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)))
11	8, 10	bitr4id 293	. . . 4 ⊢ (𝜑 → (𝑌 ∥ 𝑋 ↔ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋))
12	7, 11	anbi12d 644	. . 3 ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)))
13		dvdsruasso.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ IDomn)
14	13	idomringd 20855	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
15		dvdsruassoi.1	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
16		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝑅) = (1r‘𝑅)
17	15, 16	1unit 20481	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝑈)
18	14, 17	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑈)
19	18	ad5antr 747	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (1r‘𝑅) ∈ 𝑈)
20		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (1r‘𝑅) → (𝑢 · 𝑋) = ((1r‘𝑅) · 𝑋))
21	20	eqeq1d 2767	. . . . . . . . . . . . 13 ⊢ (𝑢 = (1r‘𝑅) → ((𝑢 · 𝑋) = 𝑌 ↔ ((1r‘𝑅) · 𝑋) = 𝑌))
22	21	adantl 487	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) ∧ 𝑢 = (1r‘𝑅)) → ((𝑢 · 𝑋) = 𝑌 ↔ ((1r‘𝑅) · 𝑋) = 𝑌))
23	14	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑅 ∈ Ring)
24	5	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑋 ∈ 𝐵)
25	1, 3, 16, 23, 24	ringlidmd 20379	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑋)
26		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑋 = (0g‘𝑅))
27	26	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 · 𝑋) = (𝑡 · (0g‘𝑅)))
28		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 · 𝑋) = 𝑌)
29		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑡 ∈ 𝐵)
30		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑅) = (0g‘𝑅)
31	1, 3, 30	ringrz 20402	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑡 ∈ 𝐵) → (𝑡 · (0g‘𝑅)) = (0g‘𝑅))
32	23, 29, 31	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 · (0g‘𝑅)) = (0g‘𝑅))
33	27, 28, 32	3eqtr3rd 2809	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (0g‘𝑅) = 𝑌)
34	25, 26, 33	3eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑌)
35	19, 22, 34	rspcedvd 3585	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
36		isidom 20852	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
37	13, 36	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
38	37	simpld 500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad5antr 747	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ CRing)
40		simp-5r 798	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑠 ∈ 𝐵)
41		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑡 ∈ 𝐵)
42	14	ad5antr 747	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ Ring)
43	1, 3, 42, 40, 41	ringcld 20362	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) ∈ 𝐵)
44	1, 16	ringidcl 20372	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
45	42, 44	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (1r‘𝑅) ∈ 𝐵)
46	5	ad5antr 747	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ 𝐵)
47		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ≠ (0g‘𝑅))
48		eldifsn 4755	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)}) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ (0g‘𝑅)))
49	46, 47, 48	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)}))
50	13	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ IDomn)
51		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑡 · 𝑋) = 𝑌)
52	51	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · (𝑡 · 𝑋)) = (𝑠 · 𝑌))
53		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑌) = 𝑋)
54	52, 53	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · (𝑡 · 𝑋)) = 𝑋)
55	1, 3, 42, 40, 41, 46	ringassd 20363	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((𝑠 · 𝑡) · 𝑋) = (𝑠 · (𝑡 · 𝑋)))
56	1, 3, 16, 42, 46	ringlidmd 20379	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑋)
57	54, 55, 56	3eqtr4d 2810	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((𝑠 · 𝑡) · 𝑋) = ((1r‘𝑅) · 𝑋))
58	1, 30, 3, 43, 45, 49, 50, 57	idomrcan 33625	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) = (1r‘𝑅))
59	42, 17	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (1r‘𝑅) ∈ 𝑈)
60	58, 59	eqeltrd 2865	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) ∈ 𝑈)
61	15, 3, 1	unitmulclb 20488	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → ((𝑠 · 𝑡) ∈ 𝑈 ↔ (𝑠 ∈ 𝑈 ∧ 𝑡 ∈ 𝑈)))
62	61	simplbda 505	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ (𝑠 · 𝑡) ∈ 𝑈) → 𝑡 ∈ 𝑈)
63	39, 40, 41, 60, 62	syl31anc 1400	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑡 ∈ 𝑈)
64		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 · 𝑋) = (𝑡 · 𝑋))
65	64	eqeq1d 2767	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑡 → ((𝑢 · 𝑋) = 𝑌 ↔ (𝑡 · 𝑋) = 𝑌))
66	65	adantl 487	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) ∧ 𝑢 = 𝑡) → ((𝑢 · 𝑋) = 𝑌 ↔ (𝑡 · 𝑋) = 𝑌))
67	63, 66, 51	rspcedvd 3585	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
68	35, 67	pm2.61dane 3047	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
69	68	r19.29an 3171	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
70	69	an32s 665	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
71	70	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) → ((𝑠 · 𝑌) = 𝑋 → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌))
72	71	an32s 665	. . . . . 6 ⊢ (((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ 𝑠 ∈ 𝐵) → ((𝑠 · 𝑌) = 𝑋 → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌))
73	72	imp 412	. . . . 5 ⊢ ((((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
74	73	r19.29an 3171	. . . 4 ⊢ (((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
75	74	anasss 472	. . 3 ⊢ ((𝜑 ∧ (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
76	12, 75	sylbida 604	. 2 ⊢ ((𝜑 ∧ (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)
77		dvdsrspss.k	. . . 4 ⊢ 𝐾 = (RSpan‘𝑅)
78	5	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑋 ∈ 𝐵)
79	9	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑌 ∈ 𝐵)
80	14	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑅 ∈ Ring)
81		simplr 781	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑢 ∈ 𝑈)
82		simpr 490	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → (𝑢 · 𝑋) = 𝑌)
83	1, 77, 2, 78, 79, 15, 3, 80, 81, 82	dvdsruassoi 33720	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋))
84	83	r19.29an 3171	. 2 ⊢ ((𝜑 ∧ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋))
85	76, 84	impbida 813	1 ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091   ∖ cdif 3903  {csn 4591   class class class wbr 5111  ‘cfv 6540  (class class class)co 7416  Basecbs 17286  ._rcmulr 17328  0_gc0g 17509  1_rcur 20286  Ringcrg 20338  CRingccrg 20339  ∥_rcdsr 20461  Unitcui 20462  Domncdomn 20820  IDomncidom 20821  RSpancrsp 21360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-1st 7988  df-2nd 7989  df-tpos 8224  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-nn 12245  df-2 12314  df-3 12315  df-sets 17241  df-slot 17259  df-ndx 17271  df-base 17287  df-ress 17308  df-plusg 17340  df-mulr 17341  df-0g 17511  df-mgm 18715  df-sgrp 18798  df-mnd 18814  df-grp 19026  df-minusg 19027  df-sbg 19028  df-cmn 19875  df-abl 19876  df-mgp 20240  df-rng 20254  df-ur 20287  df-ring 20340  df-cring 20341  df-oppr 20444  df-dvdsr 20464  df-unit 20465  df-invr 20495  df-nzr 20639  df-domn 20823  df-idom 20824

This theorem is used by:  dvdsruasso2  33722  rprmasso3  33840