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

Metamath Proof Explorer

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 drngmulrcan ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) · ( 𝐼 ‘ 𝑋 ) ) )