rhmsubcALTVlem3

Description: Lemma 3 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	$⊢ φ \to U \in V$
	rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
	rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
	rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
Assertion	rhmsubcALTVlem3	$⊢ (φ \land x \in R) \to Id (RngCatALTV (U)) (x) \in (x H x)$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$⊢ φ \to U \in V$
2		rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
3		rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
4		rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
5	3	eleq2d	$⊢ φ \to (x \in R \leftrightarrow x \in (Ring \cap U))$
6		elinel1	$⊢ x \in (Ring \cap U) \to x \in Ring$
7	5 6	biimtrdi	$⊢ φ \to (x \in R \to x \in Ring)$
8	7	imp	$⊢ (φ \land x \in R) \to x \in Ring$
9		eqid	$⊢ {Base}_{x} = {Base}_{x}$
10	9	idrhm	$⊢ x \in Ring \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
11	8 10	syl	$⊢ (φ \land x \in R) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
12	1	adantr	$⊢ (φ \land x \in R) \to U \in V$
13		eqid	$⊢ RngCatALTV (U) = RngCatALTV (U)$
14		eqid	$⊢ {Base}_{RngCatALTV (U)} = {Base}_{RngCatALTV (U)}$
15	13 14	rngccatidALTV	$⊢ U \in V \to (RngCatALTV (U) \in Cat \land Id (RngCatALTV (U)) = (y \in {Base}_{RngCatALTV (U)} ⟼ {I ↾}_{{Base}_{y}}))$
16		simpr	$⊢ (RngCatALTV (U) \in Cat \land Id (RngCatALTV (U)) = (y \in {Base}_{RngCatALTV (U)} ⟼ {I ↾}_{{Base}_{y}})) \to Id (RngCatALTV (U)) = (y \in {Base}_{RngCatALTV (U)} ⟼ {I ↾}_{{Base}_{y}})$
17	12 15 16	3syl	$⊢ (φ \land x \in R) \to Id (RngCatALTV (U)) = (y \in {Base}_{RngCatALTV (U)} ⟼ {I ↾}_{{Base}_{y}})$
18		fveq2	$⊢ y = x \to {Base}_{y} = {Base}_{x}$
19	18	reseq2d	$⊢ y = x \to {I ↾}_{{Base}_{y}} = {I ↾}_{{Base}_{x}}$
20	19	adantl	$⊢ ((φ \land x \in R) \land y = x) \to {I ↾}_{{Base}_{y}} = {I ↾}_{{Base}_{x}}$
21		incom	$⊢ Ring \cap U = U \cap Ring$
22	3 21	eqtrdi	$⊢ φ \to R = U \cap Ring$
23	22	eleq2d	$⊢ φ \to (x \in R \leftrightarrow x \in (U \cap Ring))$
24		ringrng	$⊢ x \in Ring \to x \in Rng$
25	24	anim2i	$⊢ (x \in U \land x \in Ring) \to (x \in U \land x \in Rng)$
26		elin	$⊢ x \in (U \cap Ring) \leftrightarrow (x \in U \land x \in Ring)$
27		elin	$⊢ x \in (U \cap Rng) \leftrightarrow (x \in U \land x \in Rng)$
28	25 26 27	3imtr4i	$⊢ x \in (U \cap Ring) \to x \in (U \cap Rng)$
29	23 28	biimtrdi	$⊢ φ \to (x \in R \to x \in (U \cap Rng))$
30	29	imp	$⊢ (φ \land x \in R) \to x \in (U \cap Rng)$
31	2	eqcomi	$⊢ RngCatALTV (U) = C$
32	31	fveq2i	$⊢ {Base}_{RngCatALTV (U)} = {Base}_{C}$
33	2 32 1	rngcbasALTV	$⊢ φ \to {Base}_{RngCatALTV (U)} = U \cap Rng$
34	33	adantr	$⊢ (φ \land x \in R) \to {Base}_{RngCatALTV (U)} = U \cap Rng$
35	30 34	eleqtrrd	$⊢ (φ \land x \in R) \to x \in {Base}_{RngCatALTV (U)}$
36		fvexd	$⊢ (φ \land x \in R) \to {Base}_{x} \in V$
37	36	resiexd	$⊢ (φ \land x \in R) \to {I ↾}_{{Base}_{x}} \in V$
38	17 20 35 37	fvmptd	$⊢ (φ \land x \in R) \to Id (RngCatALTV (U)) (x) = {I ↾}_{{Base}_{x}}$
39	1 2 3 4	rhmsubcALTVlem2	$⊢ (φ \land x \in R \land x \in R) \to x H x = x RingHom x$
40	39	3anidm23	$⊢ (φ \land x \in R) \to x H x = x RingHom x$
41	11 38 40	3eltr4d	$⊢ (φ \land x \in R) \to Id (RngCatALTV (U)) (x) \in (x H x)$

Metamath Proof Explorer

Theorem rhmsubcALTVlem3

Proof