Theorem drngmulcan2ad

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad analog). (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Hypotheses	drngmulcanad.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmulcanad.0	⊢ 0 = ( 0g ‘ 𝑅 )
	drngmulcanad.t	⊢ · = ( .r ‘ 𝑅 )
	drngmulcanad.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	drngmulcanad.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	drngmulcanad.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	drngmulcanad.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	drngmulcanad.1	⊢ ( 𝜑 → 𝑍 ≠ 0 )
	drngmulcan2ad.2	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
Assertion	drngmulcan2ad	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		drngmulcanad.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmulcanad.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngmulcanad.t	⊢ · = ( .r ‘ 𝑅 )
4		drngmulcanad.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		drngmulcanad.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		drngmulcanad.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		drngmulcanad.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		drngmulcanad.1	⊢ ( 𝜑 → 𝑍 ≠ 0 )
9		drngmulcan2ad.2	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
10	9	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( ( 𝑌 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
11	4	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
12		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
13	1 2 12 4 7 8	drnginvrcld	⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
14	1 3 11 5 7 13	ringassd	⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 𝑋 · ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
15		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16	1 2 3 15 12 4 7 8	drnginvrrd	⊢ ( 𝜑 → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( 𝑋 · ( 1r ‘ 𝑅 ) ) )
18	1 3 15 11 5	ringridmd	⊢ ( 𝜑 → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
19	14 17 18	3eqtrd	⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = 𝑋 )
20	1 3 11 6 7 13	ringassd	⊢ ( 𝜑 → ( ( 𝑌 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 𝑌 · ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
21	16	oveq2d	⊢ ( 𝜑 → ( 𝑌 · ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( 𝑌 · ( 1r ‘ 𝑅 ) ) )
22	1 3 15 11 6	ringridmd	⊢ ( 𝜑 → ( 𝑌 · ( 1r ‘ 𝑅 ) ) = 𝑌 )
23	20 21 22	3eqtrd	⊢ ( 𝜑 → ( ( 𝑌 · 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = 𝑌 )
24	10 19 23	3eqtr3d	⊢ ( 𝜑 → 𝑋 = 𝑌 )