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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
rng1zr.p ⊢ + = ( +g ‘ 𝑅 )
rng1zr.t ⊢ ∗ = ( .r ‘ 𝑅 )
Assertion rng1zrlem ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 rng1zr.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rng1zr.p ⊢ + = ( +g ‘ 𝑅 )
3 rng1zr.t ⊢ ∗ = ( .r ‘ 𝑅 )
4 pm4.24 ⊢ ( 𝐵 = { 𝑍 } ↔ ( 𝐵 = { 𝑍 } ∧ 𝐵 = { 𝑍 } ) )
5 simp1l ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → 𝑅 ∈ Mgm )
6 simp3 ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
7 simpl ⊢ ( ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → + Fn ( 𝐵 × 𝐵 ) )
8 7 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → + Fn ( 𝐵 × 𝐵 ) )
9 1 2 mgmb1mgm1 ⊢ ( ( 𝑅 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
10 5 6 8 9 syl3anc ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
11 simp1r ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
12 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
13 12 3 mgpplusg ⊢ ∗ = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
14 13 fneq1i ⊢ ( ∗ Fn ( 𝐵 × 𝐵 ) ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
15 14 biimpi ⊢ ( ∗ Fn ( 𝐵 × 𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
16 15 adantl ⊢ ( ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
17 16 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
18 12 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
19 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
20 18 19 mgmb1mgm1 ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
21 11 6 17 20 syl3anc ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
22 13 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ∗
23 22 a1i ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ∗ )
24 23 eqeq1d ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ↔ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
25 21 24 bitrd ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
26 10 25 anbi12d ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝐵 = { 𝑍 } ∧ 𝐵 = { 𝑍 } ) ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
27 4 26 bitrid ⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )