Metamath Proof Explorer


Theorem funcringcsetclem7ALTV

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

Ref Expression
Hypotheses funcringcsetcALTV.r 𝑅 = ( RingCatALTV ‘ 𝑈 )
funcringcsetcALTV.s 𝑆 = ( SetCat ‘ 𝑈 )
funcringcsetcALTV.b 𝐵 = ( Base ‘ 𝑅 )
funcringcsetcALTV.c 𝐶 = ( Base ‘ 𝑆 )
funcringcsetcALTV.u ( 𝜑𝑈 ∈ WUni )
funcringcsetcALTV.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcringcsetcALTV.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
Assertion funcringcsetclem7ALTV ( ( 𝜑𝑋𝐵 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV.r 𝑅 = ( RingCatALTV ‘ 𝑈 )
2 funcringcsetcALTV.s 𝑆 = ( SetCat ‘ 𝑈 )
3 funcringcsetcALTV.b 𝐵 = ( Base ‘ 𝑅 )
4 funcringcsetcALTV.c 𝐶 = ( Base ‘ 𝑆 )
5 funcringcsetcALTV.u ( 𝜑𝑈 ∈ WUni )
6 funcringcsetcALTV.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcringcsetcALTV.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
8 1 2 3 4 5 6 7 funcringcsetclem5ALTV ( ( 𝜑 ∧ ( 𝑋𝐵𝑋𝐵 ) ) → ( 𝑋 𝐺 𝑋 ) = ( I ↾ ( 𝑋 RingHom 𝑋 ) ) )
9 8 anabsan2 ( ( 𝜑𝑋𝐵 ) → ( 𝑋 𝐺 𝑋 ) = ( I ↾ ( 𝑋 RingHom 𝑋 ) ) )
10 eqid ( Id ‘ 𝑅 ) = ( Id ‘ 𝑅 )
11 5 adantr ( ( 𝜑𝑋𝐵 ) → 𝑈 ∈ WUni )
12 simpr ( ( 𝜑𝑋𝐵 ) → 𝑋𝐵 )
13 eqid ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
14 1 3 10 11 12 13 ringcidALTV ( ( 𝜑𝑋𝐵 ) → ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
15 9 14 fveq12d ( ( 𝜑𝑋𝐵 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( I ↾ ( 𝑋 RingHom 𝑋 ) ) ‘ ( I ↾ ( Base ‘ 𝑋 ) ) ) )
16 1 3 5 ringcbasALTV ( 𝜑𝐵 = ( 𝑈 ∩ Ring ) )
17 16 eleq2d ( 𝜑 → ( 𝑋𝐵𝑋 ∈ ( 𝑈 ∩ Ring ) ) )
18 elin ( 𝑋 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑋𝑈𝑋 ∈ Ring ) )
19 18 simprbi ( 𝑋 ∈ ( 𝑈 ∩ Ring ) → 𝑋 ∈ Ring )
20 17 19 syl6bi ( 𝜑 → ( 𝑋𝐵𝑋 ∈ Ring ) )
21 20 imp ( ( 𝜑𝑋𝐵 ) → 𝑋 ∈ Ring )
22 13 idrhm ( 𝑋 ∈ Ring → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ ( 𝑋 RingHom 𝑋 ) )
23 fvresi ( ( I ↾ ( Base ‘ 𝑋 ) ) ∈ ( 𝑋 RingHom 𝑋 ) → ( ( I ↾ ( 𝑋 RingHom 𝑋 ) ) ‘ ( I ↾ ( Base ‘ 𝑋 ) ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
24 21 22 23 3syl ( ( 𝜑𝑋𝐵 ) → ( ( I ↾ ( 𝑋 RingHom 𝑋 ) ) ‘ ( I ↾ ( Base ‘ 𝑋 ) ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
25 1 2 3 4 5 6 funcringcsetclem1ALTV ( ( 𝜑𝑋𝐵 ) → ( 𝐹𝑋 ) = ( Base ‘ 𝑋 ) )
26 25 fveq2d ( ( 𝜑𝑋𝐵 ) → ( ( Id ‘ 𝑆 ) ‘ ( 𝐹𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( Base ‘ 𝑋 ) ) )
27 eqid ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
28 1 3 5 ringcbasbasALTV ( ( 𝜑𝑋𝐵 ) → ( Base ‘ 𝑋 ) ∈ 𝑈 )
29 2 27 11 28 setcid ( ( 𝜑𝑋𝐵 ) → ( ( Id ‘ 𝑆 ) ‘ ( Base ‘ 𝑋 ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
30 26 29 eqtr2d ( ( 𝜑𝑋𝐵 ) → ( I ↾ ( Base ‘ 𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹𝑋 ) ) )
31 15 24 30 3eqtrd ( ( 𝜑𝑋𝐵 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹𝑋 ) ) )