Metamath Proof Explorer

Theorem rngqiprnglinlem1

Description: Lemma 1 for rngqiprnglin . (Contributed by AV, 28-Feb-2025) (Proof shortened by AV, 24-Mar-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
Assertion rngqiprnglinlem1 
|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. ( .1. .x. C ) ) = ( .1. .x. ( A .x. C ) ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 2 adantr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> I e. ( 2Ideal ` R ) )
9 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
10 8 9 syl 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> .x. = ( .r ` J ) )
11 10 oveqd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. .1. ) = ( ( .1. .x. A ) ( .r ` J ) .1. ) )
12 eqid 
 |-  ( Base ` J ) = ( Base ` J )
13 eqid 
 |-  ( .r ` J ) = ( .r ` J )
14 4 adantr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> J e. Ring )
15 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ A e. B ) -> ( .1. .x. A ) e. ( Base ` J ) )
16 15 adantrr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. A ) e. ( Base ` J ) )
17 12 13 7 14 16 ringridmd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) ( .r ` J ) .1. ) = ( .1. .x. A ) )
18 11 17 eqtrd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. .1. ) = ( .1. .x. A ) )
19 18 oveq1d 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( ( .1. .x. A ) .x. .1. ) .x. C ) = ( ( .1. .x. A ) .x. C ) )
20 1 adantr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> R e. Rng )
21 1 2 3 4 5 6 7 rngqiprng1elbas 
 |-  ( ph -> .1. e. B )
22 21 adantr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> .1. e. B )
23 simprl 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> A e. B )
24 5 6 rngcl 
 |-  ( ( R e. Rng /\ .1. e. B /\ A e. B ) -> ( .1. .x. A ) e. B )
25 20 22 23 24 syl3anc 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. A ) e. B )
26 simprr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> C e. B )
27 5 6 rngass 
 |-  ( ( R e. Rng /\ ( ( .1. .x. A ) e. B /\ .1. e. B /\ C e. B ) ) -> ( ( ( .1. .x. A ) .x. .1. ) .x. C ) = ( ( .1. .x. A ) .x. ( .1. .x. C ) ) )
28 20 25 22 26 27 syl13anc 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( ( .1. .x. A ) .x. .1. ) .x. C ) = ( ( .1. .x. A ) .x. ( .1. .x. C ) ) )
29 5 6 rngass 
 |-  ( ( R e. Rng /\ ( .1. e. B /\ A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. C ) = ( .1. .x. ( A .x. C ) ) )
30 20 22 23 26 29 syl13anc 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. C ) = ( .1. .x. ( A .x. C ) ) )
31 19 28 30 3eqtr3d 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) .x. ( .1. .x. C ) ) = ( .1. .x. ( A .x. C ) ) )