Theorem ringcinvALTV 43827

Description: An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ringcsectALTV.c	⊢ 𝐶 = (RingCatALTV‘𝑈)
ringcsectALTV.b	⊢ 𝐵 = (Base‘𝐶)
ringcsectALTV.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
ringcsectALTV.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
ringcsectALTV.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
ringcinvALTV.n	⊢ 𝑁 = (Inv‘𝐶)

Assertion

Ref	Expression
ringcinvALTV	⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))

Proof of Theorem ringcinvALTV

Step	Hyp	Ref	Expression
1		ringcsectALTV.b	. . 3 ⊢ 𝐵 = (Base‘𝐶)
2		ringcinvALTV.n	. . 3 ⊢ 𝑁 = (Inv‘𝐶)
3		ringcsectALTV.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
4		ringcsectALTV.c	. . . . 5 ⊢ 𝐶 = (RingCatALTV‘𝑈)
5	4	ringccatALTV 43824	. . . 4 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
6	3, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
7		ringcsectALTV.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		ringcsectALTV.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9		eqid 2797	. . 3 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
10	1, 2, 6, 7, 8, 9	isinv 16863	. 2 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)𝐺 ∧ 𝐺(𝑌(Sect‘𝐶)𝑋)𝐹)))
11		eqid 2797	. . . . . 6 ⊢ (Base‘𝑋) = (Base‘𝑋)
12	4, 1, 3, 7, 8, 11, 9	ringcsectALTV 43826	. . . . 5 ⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))))
13		df-3an 1082	. . . . 5 ⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))))
14	12, 13	syl6bb 288	. . . 4 ⊢ (𝜑 → (𝐹(𝑋(Sect‘𝐶)𝑌)𝐺 ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))))
15		eqid 2797	. . . . . 6 ⊢ (Base‘𝑌) = (Base‘𝑌)
16	4, 1, 3, 8, 7, 15, 9	ringcsectALTV 43826	. . . . 5 ⊢ (𝜑 → (𝐺(𝑌(Sect‘𝐶)𝑋)𝐹 ↔ (𝐺 ∈ (𝑌 RingHom 𝑋) ∧ 𝐹 ∈ (𝑋 RingHom 𝑌) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))))
17		3ancoma 1091	. . . . . 6 ⊢ ((𝐺 ∈ (𝑌 RingHom 𝑋) ∧ 𝐹 ∈ (𝑋 RingHom 𝑌) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))
18		df-3an 1082	. . . . . 6 ⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))
19	17, 18	bitri 276	. . . . 5 ⊢ ((𝐺 ∈ (𝑌 RingHom 𝑋) ∧ 𝐹 ∈ (𝑋 RingHom 𝑌) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))
20	16, 19	syl6bb 288	. . . 4 ⊢ (𝜑 → (𝐺(𝑌(Sect‘𝐶)𝑋)𝐹 ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))))
21	14, 20	anbi12d 630	. . 3 ⊢ (𝜑 → ((𝐹(𝑋(Sect‘𝐶)𝑌)𝐺 ∧ 𝐺(𝑌(Sect‘𝐶)𝑋)𝐹) ↔ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))))
22		anandi 672	. . 3 ⊢ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) ↔ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))))
23	21, 22	syl6bb 288	. 2 ⊢ (𝜑 → ((𝐹(𝑋(Sect‘𝐶)𝑌)𝐺 ∧ 𝐺(𝑌(Sect‘𝐶)𝑋)𝐹) ↔ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))))
24		simplrl 773	. . . . . 6 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → 𝐹 ∈ (𝑋 RingHom 𝑌))
25	24	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → 𝐹 ∈ (𝑋 RingHom 𝑌))
26	11, 15	rhmf 19172	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝑋 RingHom 𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))
27	15, 11	rhmf 19172	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑌 RingHom 𝑋) → 𝐺:(Base‘𝑌)⟶(Base‘𝑋))
28	26, 27	anim12i 612	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) → (𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)))
29	28	ad2antlr 723	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → (𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)))
30		simpr 485	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))) → (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))
31	30	adantl 482	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))
32		simpr 485	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) → (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))
33	32	ad2antrl 724	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))
34	31, 33	jca 512	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → ((𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))))
35	29, 34	jca 512	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) → ((𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))))
36	35	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → ((𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))))
37		fcof1o 6924	. . . . . . 7 ⊢ (((𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))) → (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ ◡𝐹 = 𝐺))
38		eqcom 2804	. . . . . . . 8 ⊢ (◡𝐹 = 𝐺 ↔ 𝐺 = ◡𝐹)
39	38	anbi2i 622	. . . . . . 7 ⊢ ((𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ ◡𝐹 = 𝐺) ↔ (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ 𝐺 = ◡𝐹))
40	37, 39	sylib 219	. . . . . 6 ⊢ (((𝐹:(Base‘𝑋)⟶(Base‘𝑌) ∧ 𝐺:(Base‘𝑌)⟶(Base‘𝑋)) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))) → (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ 𝐺 = ◡𝐹))
41	36, 40	syl 17	. . . . 5 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ 𝐺 = ◡𝐹))
42		anass 469	. . . . 5 ⊢ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌)) ∧ 𝐺 = ◡𝐹) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) ∧ 𝐺 = ◡𝐹)))
43	25, 41, 42	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌)) ∧ 𝐺 = ◡𝐹))
44	7, 8	jca 512	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
45	11, 15	isrim 19179	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹 ∈ (𝑋 RingIso 𝑌) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌))))
46	44, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ (𝑋 RingIso 𝑌) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌))))
47	46	anbi1d 629	. . . . 5 ⊢ (𝜑 → ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌)) ∧ 𝐺 = ◡𝐹)))
48	47	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹) ↔ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌)) ∧ 𝐺 = ◡𝐹)))
49	43, 48	mpbird 258	. . 3 ⊢ ((𝜑 ∧ ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))) → (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹))
50	11, 15	rimrhm 19181	. . . . . 6 ⊢ (𝐹 ∈ (𝑋 RingIso 𝑌) → 𝐹 ∈ (𝑋 RingHom 𝑌))
51	50	ad2antrl 724	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → 𝐹 ∈ (𝑋 RingHom 𝑌))
52		isrim0 19169	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹 ∈ (𝑋 RingIso 𝑌) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋))))
53	44, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∈ (𝑋 RingIso 𝑌) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋))))
54		eleq1 2872	. . . . . . . . . . . 12 ⊢ (◡𝐹 = 𝐺 → (◡𝐹 ∈ (𝑌 RingHom 𝑋) ↔ 𝐺 ∈ (𝑌 RingHom 𝑋)))
55	54	eqcoms 2805	. . . . . . . . . . 11 ⊢ (𝐺 = ◡𝐹 → (◡𝐹 ∈ (𝑌 RingHom 𝑋) ↔ 𝐺 ∈ (𝑌 RingHom 𝑋)))
56	55	anbi2d 628	. . . . . . . . . 10 ⊢ (𝐺 = ◡𝐹 → ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋)) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))))
57	53, 56	sylan9bbr 511	. . . . . . . . 9 ⊢ ((𝐺 = ◡𝐹 ∧ 𝜑) → (𝐹 ∈ (𝑋 RingIso 𝑌) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))))
58		simpr 485	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) → 𝐺 ∈ (𝑌 RingHom 𝑋))
59	57, 58	syl6bi 254	. . . . . . . 8 ⊢ ((𝐺 = ◡𝐹 ∧ 𝜑) → (𝐹 ∈ (𝑋 RingIso 𝑌) → 𝐺 ∈ (𝑌 RingHom 𝑋)))
60	59	com12 32	. . . . . . 7 ⊢ (𝐹 ∈ (𝑋 RingIso 𝑌) → ((𝐺 = ◡𝐹 ∧ 𝜑) → 𝐺 ∈ (𝑌 RingHom 𝑋)))
61	60	expdimp 453	. . . . . 6 ⊢ ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹) → (𝜑 → 𝐺 ∈ (𝑌 RingHom 𝑋)))
62	61	impcom 408	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → 𝐺 ∈ (𝑌 RingHom 𝑋))
63		coeq1 5621	. . . . . . 7 ⊢ (𝐺 = ◡𝐹 → (𝐺 ∘ 𝐹) = (◡𝐹 ∘ 𝐹))
64	63	ad2antll 725	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐺 ∘ 𝐹) = (◡𝐹 ∘ 𝐹))
65	11, 15	rimf1o 19180	. . . . . . . 8 ⊢ (𝐹 ∈ (𝑋 RingIso 𝑌) → 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌))
66	65	ad2antrl 724	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → 𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌))
67		f1ococnv1 6518	. . . . . . 7 ⊢ (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) → (◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))
68	66, 67	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))
69	64, 68	eqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋)))
70	51, 62, 69	jca31 515	. . . 4 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))))
71	53	biimpcd 250	. . . . . . 7 ⊢ (𝐹 ∈ (𝑋 RingIso 𝑌) → (𝜑 → (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋))))
72	71	adantr 481	. . . . . 6 ⊢ ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹) → (𝜑 → (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋))))
73	72	impcom 408	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋)))
74		eleq1 2872	. . . . . . 7 ⊢ (𝐺 = ◡𝐹 → (𝐺 ∈ (𝑌 RingHom 𝑋) ↔ ◡𝐹 ∈ (𝑌 RingHom 𝑋)))
75	74	ad2antll 725	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐺 ∈ (𝑌 RingHom 𝑋) ↔ ◡𝐹 ∈ (𝑌 RingHom 𝑋)))
76	75	anbi2d 628	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → ((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ ◡𝐹 ∈ (𝑌 RingHom 𝑋))))
77	73, 76	mpbird 258	. . . 4 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)))
78		coeq2 5622	. . . . . . 7 ⊢ (𝐺 = ◡𝐹 → (𝐹 ∘ 𝐺) = (𝐹 ∘ ◡𝐹))
79	78	ad2antll 725	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐹 ∘ 𝐺) = (𝐹 ∘ ◡𝐹))
80		f1ococnv2 6516	. . . . . . 7 ⊢ (𝐹:(Base‘𝑋)–1-1-onto→(Base‘𝑌) → (𝐹 ∘ ◡𝐹) = ( I ↾ (Base‘𝑌)))
81	66, 80	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐹 ∘ ◡𝐹) = ( I ↾ (Base‘𝑌)))
82	79, 81	eqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))
83	77, 69, 82	jca31 515	. . . 4 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌))))
84	70, 77, 83	jca31 515	. . 3 ⊢ ((𝜑 ∧ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)) → ((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))))
85	49, 84	impbida 797	. 2 ⊢ (𝜑 → (((((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋))) ∧ (((𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋)) ∧ (𝐺 ∘ 𝐹) = ( I ↾ (Base‘𝑋))) ∧ (𝐹 ∘ 𝐺) = ( I ↾ (Base‘𝑌)))) ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))
86	10, 23, 85	3bitrd 306	1 ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083   class class class wbr 4968   I cid 5354  ^◡ccnv 5449   ↾ cres 5452   ∘ ccom 5454  ⟶wf 6228  –1-1-onto→wf1o 6231  ‘cfv 6232  (class class class)co 7023  Basecbs 16316  Catccat 16768  Sectcsect 16847  Invcinv 16848   RingHom crh 19158   RingIso crs 19159  RingCatALTVcringcALTV 43775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-z 11836  df-dec 11953  df-uz 12098  df-fz 12747  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-plusg 16411  df-hom 16422  df-cco 16423  df-0g 16548  df-cat 16772  df-cid 16773  df-sect 16850  df-inv 16851  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-mhm 17778  df-grp 17868  df-ghm 18101  df-mgp 18934  df-ur 18946  df-ring 18993  df-rnghom 19161  df-rngiso 19162  df-ringcALTV 43777

This theorem is referenced by:  ringcisoALTV  43828