Theorem dvdsruasso2

Description: A reformulation of dvdsruasso . (Proposed by Gerard Lang, 28-May-2025.) (Contributed by Thiery Arnoux, 29-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		dvdsruassoi.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
7		dvdsruassoi.2	⊢ · = ( .r ‘ 𝑅 )
8		dvdsruasso.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
9		dvdsruasso2.1	⊢ 1 = ( 1r ‘ 𝑅 )
10	1 2 3 4 5 6 7 8	dvdsruasso	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) )
11		oveq1	⊢ ( 𝑣 = ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) → ( 𝑣 · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) )
12	11	eqeq1d	⊢ ( 𝑣 = ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) → ( ( 𝑣 · 𝑌 ) = 𝑋 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) = 𝑋 ) )
13		oveq2	⊢ ( 𝑣 = ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) → ( 𝑢 · 𝑣 ) = ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) )
14	13	eqeq1d	⊢ ( 𝑣 = ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) → ( ( 𝑢 · 𝑣 ) = 1 ↔ ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) = 1 ) )
15	12 14	3anbi23d	⊢ ( 𝑣 = ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) → ( ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ↔ ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) = 𝑋 ∧ ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) = 1 ) ) )
16	8	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
17	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑅 ∈ Ring )
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑢 ∈ 𝑈 )
19		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
20	6 19	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ∈ 𝑈 )
21	17 18 20	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ∈ 𝑈 )
22		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 𝑢 · 𝑋 ) = 𝑌 )
23	22	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · ( 𝑢 · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) )
24	8	idomcringd	⊢ ( 𝜑 → 𝑅 ∈ CRing )
25	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑅 ∈ CRing )
26	1 6	unitcl	⊢ ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ∈ 𝑈 → ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ∈ 𝐵 )
27	21 26	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ∈ 𝐵 )
28	1 6	unitcl	⊢ ( 𝑢 ∈ 𝑈 → 𝑢 ∈ 𝐵 )
29	18 28	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑢 ∈ 𝐵 )
30	1 7 25 27 29	crngcomd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑢 ) = ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) )
31	6 19 7 9	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) = 1 )
32	17 18 31	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) = 1 )
33	30 32	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑢 ) = 1 )
34	33	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑢 ) · 𝑋 ) = ( 1 · 𝑋 ) )
35	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
36	1 7 17 27 29 35	ringassd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑢 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · ( 𝑢 · 𝑋 ) ) )
37	1 7 9 17 35	ringlidmd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 1 · 𝑋 ) = 𝑋 )
38	34 36 37	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · ( 𝑢 · 𝑋 ) ) = 𝑋 )
39	23 38	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) = 𝑋 )
40	22 39 32	3jca	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) · 𝑌 ) = 𝑋 ∧ ( 𝑢 · ( ( invr ‘ 𝑅 ) ‘ 𝑢 ) ) = 1 ) )
41	15 21 40	rspcedvdw	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) )
42		simpr1	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ) → ( 𝑢 · 𝑋 ) = 𝑌 )
43	42	r19.29an	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ) → ( 𝑢 · 𝑋 ) = 𝑌 )
44	41 43	impbida	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 𝑢 · 𝑋 ) = 𝑌 ↔ ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ) )
45	44	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ↔ ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ) )
46	10 45	bitrd	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 · 𝑋 ) = 𝑌 ∧ ( 𝑣 · 𝑌 ) = 𝑋 ∧ ( 𝑢 · 𝑣 ) = 1 ) ) )