Metamath Proof Explorer

Theorem isrngisom

Description: An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020)

Ref Expression
Assertion isrngisom ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-rngisom ⊢ RngIsom = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RngHomo 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RngHomo 𝑟 ) } )
2 1 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → RngIsom = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RngHomo 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RngHomo 𝑟 ) } ) )
3 oveq12 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 RngHomo 𝑠 ) = ( 𝑅 RngHomo 𝑆 ) )
4 3 adantl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( 𝑟 RngHomo 𝑠 ) = ( 𝑅 RngHomo 𝑆 ) )
5 oveq12 ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑠 RngHomo 𝑟 ) = ( 𝑆 RngHomo 𝑅 ) )
6 5 ancoms ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑠 RngHomo 𝑟 ) = ( 𝑆 RngHomo 𝑅 ) )
7 6 adantl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 RngHomo 𝑟 ) = ( 𝑆 RngHomo 𝑅 ) )
8 7 eleq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( ◡ 𝑓 ∈ ( 𝑠 RngHomo 𝑟 ) ↔ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) ) )
9 4 8 rabeqbidv ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → { 𝑓 ∈ ( 𝑟 RngHomo 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RngHomo 𝑟 ) } = { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } )
10 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
11 10 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝑅 ∈ V )
12 elex ⊢ ( 𝑆 ∈ 𝑊 → 𝑆 ∈ V )
13 12 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝑆 ∈ V )
14 ovex ⊢ ( 𝑅 RngHomo 𝑆 ) ∈ V
15 14 rabex ⊢ { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } ∈ V
16 15 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } ∈ V )
17 2 9 11 13 16 ovmpod ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 RngIsom 𝑆 ) = { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } )
18 17 eleq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } ) )
19 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
20 19 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) ↔ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) )
21 20 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RngHomo 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RngHomo 𝑅 ) } ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) )
22 18 21 bitrdi ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) ) )