Metamath Proof Explorer

Theorem rprmasso2

Description: In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmasso.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmasso.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmasso.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
rprmasso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
rprmasso.1 ⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
rprmasso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
Assertion rprmasso2 ( 𝜑 → 𝑌 ∥ 𝑋 )

Proof

Step Hyp Ref Expression
1 rprmasso.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmasso.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 rprmasso.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 rprmasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 rprmasso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 rprmasso.1 ⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
7 rprmasso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑅 ∈ IDomn )
10 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑌 ∈ 𝑃 )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑡 ∈ 𝐵 )
12 1 2 4 5 rprmcl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
14 4 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
15 1 2 4 7 rprmcl ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
16 1 3 dvdsrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∥ 𝑌 )
17 14 15 16 syl2anc ⊢ ( 𝜑 → 𝑌 ∥ 𝑌 )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑌 ∥ 𝑌 )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 )
20 18 19 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑌 ∥ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) )
21 1 2 3 8 9 10 11 13 20 rprmdvds ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → ( 𝑌 ∥ 𝑡 ∨ 𝑌 ∥ 𝑋 ) )
22 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → 𝑋 ∈ 𝐵 )
23 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24 11 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑡 ∈ 𝐵 )
25 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → 𝑡 = ( 0g ‘ 𝑅 ) )
26 25 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) )
27 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 )
28 1 8 23 14 12 ringlzd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
29 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
30 26 27 29 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → 𝑌 = ( 0g ‘ 𝑅 ) )
31 2 23 4 7 rprmnz ⊢ ( 𝜑 → 𝑌 ≠ ( 0g ‘ 𝑅 ) )
32 31 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → 𝑌 ≠ ( 0g ‘ 𝑅 ) )
33 32 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑡 = ( 0g ‘ 𝑅 ) ) → ¬ 𝑌 = ( 0g ‘ 𝑅 ) )
34 30 33 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → ¬ 𝑡 = ( 0g ‘ 𝑅 ) )
35 34 neqned ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑡 ≠ ( 0g ‘ 𝑅 ) )
36 35 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑡 ≠ ( 0g ‘ 𝑅 ) )
37 24 36 eldifsnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑡 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
38 14 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑅 ∈ Ring )
39 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑢 ∈ 𝐵 )
40 13 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑋 ∈ 𝐵 )
41 1 8 38 39 40 ringcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 )
42 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
43 1 42 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
44 14 43 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
45 44 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
46 4 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
47 46 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑅 ∈ Domn )
48 19 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 )
49 48 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) )
50 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 )
51 49 50 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) ) = 𝑡 )
52 4 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
53 52 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → 𝑅 ∈ CRing )
54 1 8 53 24 39 40 crng12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑡 ( .r ‘ 𝑅 ) ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) ) )
55 1 8 42 38 24 ringridmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑡 )
56 51 54 55 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑡 ( .r ‘ 𝑅 ) ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
57 1 23 8 37 41 45 47 56 domnlcan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) → ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
58 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → 𝑌 ∈ 𝐵 )
59 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → 𝑌 ∥ 𝑡 )
60 1 3 8 dvdsr2 ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑌 ∥ 𝑡 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 ) )
61 60 biimpa ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑌 ∥ 𝑡 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 )
62 58 59 61 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑡 )
63 57 62 reximddv3 ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
64 1 3 8 dvdsr2 ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∥ ( 1r ‘ 𝑅 ) ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) ) )
65 64 biimpar ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) ) → 𝑋 ∥ ( 1r ‘ 𝑅 ) )
66 22 63 65 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → 𝑋 ∥ ( 1r ‘ 𝑅 ) )
67 42 3 2 52 5 rprmndvdsr1 ⊢ ( 𝜑 → ¬ 𝑋 ∥ ( 1r ‘ 𝑅 ) )
68 67 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ∧ 𝑌 ∥ 𝑡 ) → ¬ 𝑋 ∥ ( 1r ‘ 𝑅 ) )
69 66 68 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → ¬ 𝑌 ∥ 𝑡 )
70 21 69 orcnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) → 𝑌 ∥ 𝑋 )
71 1 3 8 dvdsr ⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) )
72 6 71 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) )
73 72 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 )
74 70 73 r19.29a ⊢ ( 𝜑 → 𝑌 ∥ 𝑋 )