funcringcsetcALTV2lem7

Description: Lemma 7 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
	funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetcALTV2lem7	$⊢ (φ \land X \in B) \to (X G X) (Id (R) (X)) = Id (S) (F (X))$

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
2		funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
8	1 2 3 4 5 6 7	funcringcsetcALTV2lem5	$⊢ (φ \land (X \in B \land X \in B)) \to X G X = {I ↾}_{(X RingHom X)}$
9	8	anabsan2	$⊢ (φ \land X \in B) \to X G X = {I ↾}_{(X RingHom X)}$
10		eqid	$⊢ Id (R) = Id (R)$
11	5	adantr	$⊢ (φ \land X \in B) \to U \in WUni$
12		simpr	$⊢ (φ \land X \in B) \to X \in B$
13		eqid	$⊢ {Base}_{X} = {Base}_{X}$
14	1 3 10 11 12 13	ringcid	$⊢ (φ \land X \in B) \to Id (R) (X) = {I ↾}_{{Base}_{X}}$
15	9 14	fveq12d	$⊢ (φ \land X \in B) \to (X G X) (Id (R) (X)) = ({I ↾}_{(X RingHom X)}) ({I ↾}_{{Base}_{X}})$
16	1 3 5	ringcbas	$⊢ φ \to B = U \cap Ring$
17	16	eleq2d	$⊢ φ \to (X \in B \leftrightarrow X \in (U \cap Ring))$
18		elin	$⊢ X \in (U \cap Ring) \leftrightarrow (X \in U \land X \in Ring)$
19	18	simprbi	$⊢ X \in (U \cap Ring) \to X \in Ring$
20	17 19	syl6bi	$⊢ φ \to (X \in B \to X \in Ring)$
21	20	imp	$⊢ (φ \land X \in B) \to X \in Ring$
22	13	idrhm	$⊢ X \in Ring \to {I ↾}_{{Base}_{X}} \in (X RingHom X)$
23		fvresi	$⊢ {I ↾}_{{Base}_{X}} \in (X RingHom X) \to ({I ↾}_{(X RingHom X)}) ({I ↾}_{{Base}_{X}}) = {I ↾}_{{Base}_{X}}$
24	21 22 23	3syl	$⊢ (φ \land X \in B) \to ({I ↾}_{(X RingHom X)}) ({I ↾}_{{Base}_{X}}) = {I ↾}_{{Base}_{X}}$
25	1 2 3 4 5 6	funcringcsetcALTV2lem1	$⊢ (φ \land X \in B) \to F (X) = {Base}_{X}$
26	25	fveq2d	$⊢ (φ \land X \in B) \to Id (S) (F (X)) = Id (S) ({Base}_{X})$
27		eqid	$⊢ Id (S) = Id (S)$
28	1 3 5	ringcbasbas	$⊢ (φ \land X \in B) \to {Base}_{X} \in U$
29	2 27 11 28	setcid	$⊢ (φ \land X \in B) \to Id (S) ({Base}_{X}) = {I ↾}_{{Base}_{X}}$
30	26 29	eqtr2d	$⊢ (φ \land X \in B) \to {I ↾}_{{Base}_{X}} = Id (S) (F (X))$
31	15 24 30	3eqtrd	$⊢ (φ \land X \in B) \to (X G X) (Id (R) (X)) = Id (S) (F (X))$

Metamath Proof Explorer

Theorem funcringcsetcALTV2lem7

Proof