Theorem drngmulcanad

Description: Cancellation of a nonzero factor on the left for multiplication. ( mulcanad 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 )
	drngmulcanad.2	⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) )
Assertion	drngmulcanad	⊢ ( 𝜑 → 𝑋 = 𝑌 )

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		drngmulcanad.2	⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) )
10	9	oveq2d	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) )
11		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
13	1 2 3 11 12 4 7 8	drnginvrld	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) = ( 1r ‘ 𝑅 ) )
14	13	oveq1d	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
15	4	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	1 2 12 4 7 8	drnginvrcld	⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
17	1 3 15 16 7 5	ringassd	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) )
18	1 3 11 15 5	ringlidmd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
19	14 17 18	3eqtr3d	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑋 ) ) = 𝑋 )
20	13	oveq1d	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑌 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
21	1 3 15 16 7 6	ringassd	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · 𝑍 ) · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) )
22	1 3 11 15 6	ringlidmd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
23	20 21 22	3eqtr3d	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( 𝑍 · 𝑌 ) ) = 𝑌 )
24	10 19 23	3eqtr3d	⊢ ( 𝜑 → 𝑋 = 𝑌 )