rngcisoALTV

Description: An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcsectALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngcsectALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	rngcsectALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcsectALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	rngcsectALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	rngcisoALTV.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion	rngcisoALTV	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngcsectALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2		rngcsectALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rngcsectALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4		rngcsectALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		rngcsectALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		rngcisoALTV.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
7		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
8	1	rngccatALTV	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
9	3 8	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
10	2 7 9 4 5 6	isoval	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
11	10	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
12	2 7 9 4 5	invfun	⊢ ( 𝜑 → Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
13		funfvbrb	⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
15	1 2 3 4 5 7	rngcinvALTV	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ^◡ 𝐹 ) ) )
16		simpl	⊢ ( ( 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ^◡ 𝐹 ) → 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) )
17	15 16	biimtrdi	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) → 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ) )
18	14 17	sylbid	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ) )
19		eqid	⊢ ^◡ 𝐹 = ^◡ 𝐹
20	1 2 3 4 5 7	rngcinvALTV	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ^◡ 𝐹 ↔ ( 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ∧ ^◡ 𝐹 = ^◡ 𝐹 ) ) )
21		funrel	⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
22	12 21	syl	⊢ ( 𝜑 → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
23		releldm	⊢ ( ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ^◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
24	23	ex	⊢ ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ^◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
25	22 24	syl	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ^◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
26	20 25	sylbird	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ∧ ^◡ 𝐹 = ^◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
27	19 26	mpan2i	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
28	18 27	impbid	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ) )
29	11 28	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngIso 𝑌 ) ) )

Metamath Proof Explorer

Theorem rngcisoALTV

Proof