rngqiprngghmlem1

	Ref	Expression
Hypotheses	rng2idlring.r	$⊢ φ \to R \in Rng$
	rng2idlring.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlring.j	$⊢ J = R ↾_{𝑠} I$
	rng2idlring.u	$⊢ φ \to J \in Ring$
	rng2idlring.b	$⊢ B = {Base}_{R}$
	rng2idlring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rng2idlring.1	$⊢ \underset{˙}{1} = 1_{J}$
Assertion	rngqiprngghmlem1	$⊢ (φ \land A \in B) \to \underset{˙}{1} \underset{˙}{\cdot} A \in {Base}_{J}$

Step	Hyp	Ref	Expression
1		rng2idlring.r	$⊢ φ \to R \in Rng$
2		rng2idlring.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlring.j	$⊢ J = R ↾_{𝑠} I$
4		rng2idlring.u	$⊢ φ \to J \in Ring$
5		rng2idlring.b	$⊢ B = {Base}_{R}$
6		rng2idlring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		rng2idlring.1	$⊢ \underset{˙}{1} = 1_{J}$
8		eqid	$⊢ {Base}_{J} = {Base}_{J}$
9	2 3 8	2idlelbas	$⊢ φ \to ({Base}_{J} \in LIdeal (R) \land {Base}_{J} \in LIdeal ({opp}_{r} (R)))$
10	9	simprd	$⊢ φ \to {Base}_{J} \in LIdeal ({opp}_{r} (R))$
11		ringrng	$⊢ J \in Ring \to J \in Rng$
12	4 11	syl	$⊢ φ \to J \in Rng$
13	3 12	eqeltrrid	$⊢ φ \to R ↾_{𝑠} I \in Rng$
14	1 2 13	rng2idl0	$⊢ φ \to 0_{R} \in I$
15	2 3 8	2idlbas	$⊢ φ \to {Base}_{J} = I$
16	14 15	eleqtrrd	$⊢ φ \to 0_{R} \in {Base}_{J}$
17	1 10 16	3jca	$⊢ φ \to (R \in Rng \land {Base}_{J} \in LIdeal ({opp}_{r} (R)) \land 0_{R} \in {Base}_{J})$
18	8 7	ringidcl	$⊢ J \in Ring \to \underset{˙}{1} \in {Base}_{J}$
19	4 18	syl	$⊢ φ \to \underset{˙}{1} \in {Base}_{J}$
20	19	anim1ci	$⊢ (φ \land A \in B) \to (A \in B \land \underset{˙}{1} \in {Base}_{J})$
21		eqid	$⊢ 0_{R} = 0_{R}$
22		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
23	21 5 6 22	rngridlmcl	$⊢ ((R \in Rng \land {Base}_{J} \in LIdeal ({opp}_{r} (R)) \land 0_{R} \in {Base}_{J}) \land (A \in B \land \underset{˙}{1} \in {Base}_{J})) \to \underset{˙}{1} \underset{˙}{\cdot} A \in {Base}_{J}$
24	17 20 23	syl2an2r	$⊢ (φ \land A \in B) \to \underset{˙}{1} \underset{˙}{\cdot} A \in {Base}_{J}$

Metamath Proof Explorer