Metamath Proof Explorer

Theorem rng1zrlem

Description: Lemma for rng1zr and srg1zr . (Contributed by FL, 13-Feb-2010) (Revised by AV, 18-Jun-2026)

Ref Expression
Hypotheses rng1zr.b 
|- B = ( Base ` R )
rng1zr.p 
|- .+ = ( +g ` R )
rng1zr.t 
|- .* = ( .r ` R )
Assertion rng1zrlem 
|- ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )

Proof

Step Hyp Ref Expression
1 rng1zr.b 
 |-  B = ( Base ` R )
2 rng1zr.p 
 |-  .+ = ( +g ` R )
3 rng1zr.t 
 |-  .* = ( .r ` R )
4 pm4.24 
 |-  ( B = { Z } <-> ( B = { Z } /\ B = { Z } ) )
5 simp1l 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> R e. Mgm )
6 simp3 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> Z e. B )
7 simpl 
 |-  ( ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> .+ Fn ( B X. B ) )
8 7 3ad2ant2 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> .+ Fn ( B X. B ) )
9 1 2 mgmb1mgm1 
 |-  ( ( R e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
10 5 6 8 9 syl3anc 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
11 simp1r 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( mulGrp ` R ) e. Mgm )
12 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
13 12 3 mgpplusg 
 |-  .* = ( +g ` ( mulGrp ` R ) )
14 13 fneq1i 
 |-  ( .* Fn ( B X. B ) <-> ( +g ` ( mulGrp ` R ) ) Fn ( B X. B ) )
15 14 biimpi 
 |-  ( .* Fn ( B X. B ) -> ( +g ` ( mulGrp ` R ) ) Fn ( B X. B ) )
16 15 adantl 
 |-  ( ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( +g ` ( mulGrp ` R ) ) Fn ( B X. B ) )
17 16 3ad2ant2 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( +g ` ( mulGrp ` R ) ) Fn ( B X. B ) )
18 12 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
19 eqid 
 |-  ( +g ` ( mulGrp ` R ) ) = ( +g ` ( mulGrp ` R ) )
20 18 19 mgmb1mgm1 
 |-  ( ( ( mulGrp ` R ) e. Mgm /\ Z e. B /\ ( +g ` ( mulGrp ` R ) ) Fn ( B X. B ) ) -> ( B = { Z } <-> ( +g ` ( mulGrp ` R ) ) = { <. <. Z , Z >. , Z >. } ) )
21 11 6 17 20 syl3anc 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( +g ` ( mulGrp ` R ) ) = { <. <. Z , Z >. , Z >. } ) )
22 13 eqcomi 
 |-  ( +g ` ( mulGrp ` R ) ) = .*
23 22 a1i 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( +g ` ( mulGrp ` R ) ) = .* )
24 23 eqeq1d 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( ( +g ` ( mulGrp ` R ) ) = { <. <. Z , Z >. , Z >. } <-> .* = { <. <. Z , Z >. , Z >. } ) )
25 21 24 bitrd 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> .* = { <. <. Z , Z >. , Z >. } ) )
26 10 25 anbi12d 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( ( B = { Z } /\ B = { Z } ) <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
27 4 26 bitrid 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )