Theorem drnginvmuld

Description: Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		drnginvmuld.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drnginvmuld.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		drnginvmuld.t	⊢ · = ( .r ‘ 𝑅 )
4		drnginvmuld.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
5		drnginvmuld.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
6		drnginvmuld.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		drnginvmuld.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		drnginvmuld.1	⊢ ( 𝜑 → 𝑋 ≠ 0 )
9		drnginvmuld.2	⊢ ( 𝜑 → 𝑌 ≠ 0 )
10	5	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
11	1 3 10 6 7	ringcld	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
12	1 2 3 5 6 7	drngmulne0	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )
13	8 9 12	mpbir2and	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ≠ 0 )
14	1 2 4 5 11 13	drnginvrcld	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐵 )
15	1 2 4 5 7 9	drnginvrcld	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑌 ) ∈ 𝐵 )
16	1 2 4 5 6 8	drnginvrcld	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
17	1 3 10 15 16	ringcld	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑌 ) · ( 𝐼 ‘ 𝑋 ) ) ∈ 𝐵 )
18		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19	1 2 3 18 4 5 6 8	drnginvrld	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
21	1 3 18 10 7	ringlidmd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
22	20 21	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) = 𝑌 )
23	22	oveq2d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑌 ) · ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) · 𝑌 ) )
24	23	eqcomd	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑌 ) · 𝑌 ) = ( ( 𝐼 ‘ 𝑌 ) · ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) ) )
25	1 2 3 18 4 5 7 9	drnginvrld	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑌 ) · 𝑌 ) = ( 1r ‘ 𝑅 ) )
26	1 3 10 16 6 7	ringassd	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) = ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑌 ) ) )
27	26	oveq2d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑌 ) · ( ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) · 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) · ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑌 ) ) ) )
28	24 25 27	3eqtr3d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( ( 𝐼 ‘ 𝑌 ) · ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑌 ) ) ) )
29	1 2 3 18 4 5 11 13	drnginvrld	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 · 𝑌 ) ) · ( 𝑋 · 𝑌 ) ) = ( 1r ‘ 𝑅 ) )
30	1 3 10 15 16 11	ringassd	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑌 ) · ( 𝐼 ‘ 𝑋 ) ) · ( 𝑋 · 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) · ( ( 𝐼 ‘ 𝑋 ) · ( 𝑋 · 𝑌 ) ) ) )
31	28 29 30	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 · 𝑌 ) ) · ( 𝑋 · 𝑌 ) ) = ( ( ( 𝐼 ‘ 𝑌 ) · ( 𝐼 ‘ 𝑋 ) ) · ( 𝑋 · 𝑌 ) ) )
32	1 2 3 5 14 17 11 13 31	drngmulcan2ad	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) · ( 𝐼 ‘ 𝑋 ) ) )