Metamath Proof Explorer

Theorem rngqiprnglin

Description: F is linear with respect to the multiplication. (Contributed by AV, 28-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion rngqiprnglin ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
5 rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
7 rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
8 rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9 rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
10 rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
11 rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
12 rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
13 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
14 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
15 9 ovexi ⊢ 𝑄 ∈ V
16 15 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑄 ∈ V )
17 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐽 ∈ Ring )
18 simpl ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
19 8 9 5 13 quseccl0 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ) → [ 𝑎 ] ∼ ∈ ( Base ‘ 𝑄 ) )
20 1 18 19 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑎 ] ∼ ∈ ( Base ‘ 𝑄 ) )
21 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 1 · 𝑎 ) ∈ ( Base ‘ 𝐽 ) )
22 18 21 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 1 · 𝑎 ) ∈ ( Base ‘ 𝐽 ) )
23 simpr ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
24 8 9 5 13 quseccl0 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵 ) → [ 𝑏 ] ∼ ∈ ( Base ‘ 𝑄 ) )
25 1 23 24 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑏 ] ∼ ∈ ( Base ‘ 𝑄 ) )
26 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 · 𝑏 ) ∈ ( Base ‘ 𝐽 ) )
27 23 26 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 1 · 𝑏 ) ∈ ( Base ‘ 𝐽 ) )
28 1 2 3 4 5 6 7 8 9 rngqiprnglinlem3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( [ 𝑎 ] ∼ ( .r ‘ 𝑄 ) [ 𝑏 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )
29 eqid ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
30 14 29 17 22 27 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 1 · 𝑎 ) ( .r ‘ 𝐽 ) ( 1 · 𝑏 ) ) ∈ ( Base ‘ 𝐽 ) )
31 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
32 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
33 11 13 14 16 17 20 22 25 27 28 30 31 29 32 xpsmul ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( .r ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) = ⟨ ( [ 𝑎 ] ∼ ( .r ‘ 𝑄 ) [ 𝑏 ] ∼ ) , ( ( 1 · 𝑎 ) ( .r ‘ 𝐽 ) ( 1 · 𝑏 ) ) ⟩ )
34 1 2 3 4 5 6 7 8 9 rngqiprnglinlem2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ ( 𝑎 · 𝑏 ) ] ∼ = ( [ 𝑎 ] ∼ ( .r ‘ 𝑄 ) [ 𝑏 ] ∼ ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( [ 𝑎 ] ∼ ( .r ‘ 𝑄 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 · 𝑏 ) ] ∼ )
36 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
37 3 6 ressmulr ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → · = ( .r ‘ 𝐽 ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → · = ( .r ‘ 𝐽 ) )
39 38 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( .r ‘ 𝐽 ) = · )
40 39 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 1 · 𝑎 ) ( .r ‘ 𝐽 ) ( 1 · 𝑏 ) ) = ( ( 1 · 𝑎 ) · ( 1 · 𝑏 ) ) )
41 1 2 3 4 5 6 7 rngqiprnglinlem1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 1 · 𝑎 ) · ( 1 · 𝑏 ) ) = ( 1 · ( 𝑎 · 𝑏 ) ) )
42 40 41 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 1 · 𝑎 ) ( .r ‘ 𝐽 ) ( 1 · 𝑏 ) ) = ( 1 · ( 𝑎 · 𝑏 ) ) )
43 35 42 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ⟨ ( [ 𝑎 ] ∼ ( .r ‘ 𝑄 ) [ 𝑏 ] ∼ ) , ( ( 1 · 𝑎 ) ( .r ‘ 𝐽 ) ( 1 · 𝑏 ) ) ⟩ = ⟨ [ ( 𝑎 · 𝑏 ) ] ∼ , ( 1 · ( 𝑎 · 𝑏 ) ) ⟩ )
44 33 43 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ⟨ [ ( 𝑎 · 𝑏 ) ] ∼ , ( 1 · ( 𝑎 · 𝑏 ) ) ⟩ = ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( .r ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) )
45 1 anim1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
46 3anass ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
47 45 46 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) )
48 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
50 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ ( 𝑎 · 𝑏 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ⟨ [ ( 𝑎 · 𝑏 ) ] ∼ , ( 1 · ( 𝑎 · 𝑏 ) ) ⟩ )
51 49 50 syldan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ⟨ [ ( 𝑎 · 𝑏 ) ] ∼ , ( 1 · ( 𝑎 · 𝑏 ) ) ⟩ )
52 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
53 18 52 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
54 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ )
55 23 54 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) = ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ )
56 53 55 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) = ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( .r ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) )
57 44 51 56 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) )
58 57 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) )