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	$⊢ \underset{˙}{+} = +_{R}$
	rng1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
Assertion	rng1zrlem	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$

Proof

Step	Hyp	Ref	Expression
1		rng1zr.b	$⊢ B = {Base}_{R}$
2		rng1zr.p	$⊢ \underset{˙}{+} = +_{R}$
3		rng1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
4		pm4.24	$⊢ B = \{Z\} \leftrightarrow (B = \{Z\} \land B = \{Z\})$
5		simp1l	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to R \in Mgm$
6		simp3	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to Z \in B$
7		simpl	$⊢ (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to \underset{˙}{+} Fn (B \times B)$
8	7	3ad2ant2	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to \underset{˙}{+} Fn (B \times B)$
9	1 2	mgmb1mgm1	$⊢ (R \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$
10	5 6 8 9	syl3anc	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$
11		simp1r	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to {mulGrp}_{R} \in Mgm$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13	12 3	mgpplusg	$⊢ \underset{˙}{*} = +_{{mulGrp}_{R}}$
14	13	fneq1i	$⊢ \underset{˙}{*} Fn (B \times B) \leftrightarrow +_{{mulGrp}_{R}} Fn (B \times B)$
15	14	biimpi	$⊢ \underset{˙}{*} Fn (B \times B) \to +_{{mulGrp}_{R}} Fn (B \times B)$
16	15	adantl	$⊢ (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to +_{{mulGrp}_{R}} Fn (B \times B)$
17	16	3ad2ant2	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to +_{{mulGrp}_{R}} Fn (B \times B)$
18	12 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
19		eqid	$⊢ +_{{mulGrp}_{R}} = +_{{mulGrp}_{R}}$
20	18 19	mgmb1mgm1	$⊢ ({mulGrp}_{R} \in Mgm \land Z \in B \land +_{{mulGrp}_{R}} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow +_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\})$
21	11 6 17 20	syl3anc	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow +_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\})$
22	13	eqcomi	$⊢ +_{{mulGrp}_{R}} = \underset{˙}{*}$
23	22	a1i	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to +_{{mulGrp}_{R}} = \underset{˙}{}$
24	23	eqeq1d	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (+_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\} \leftrightarrow \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\})$
25	21 24	bitrd	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\})$
26	10 25	anbi12d	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to ((B = \{Z\} \land B = \{Z\}) \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$
27	4 26	bitrid	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \land (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$

Metamath Proof Explorer

Theorem rng1zrlem

Proof