This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )