Metamath Proof Explorer

Theorem rnghmsubcsetclem1

Description: Lemma 1 for rnghmsubcsetc . (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rnghmsubcsetc.c 
|- C = ( ExtStrCat ` U )
rnghmsubcsetc.u 
|- ( ph -> U e. V )
rnghmsubcsetc.b 
|- ( ph -> B = ( Rng i^i U ) )
rnghmsubcsetc.h 
|- ( ph -> H = ( RngHom |` ( B X. B ) ) )
Assertion rnghmsubcsetclem1 
|- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )

Proof

Step Hyp Ref Expression
1 rnghmsubcsetc.c 
 |-  C = ( ExtStrCat ` U )
2 rnghmsubcsetc.u 
 |-  ( ph -> U e. V )
3 rnghmsubcsetc.b 
 |-  ( ph -> B = ( Rng i^i U ) )
4 rnghmsubcsetc.h 
 |-  ( ph -> H = ( RngHom |` ( B X. B ) ) )
5 3 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Rng i^i U ) ) )
6 elin 
 |-  ( x e. ( Rng i^i U ) <-> ( x e. Rng /\ x e. U ) )
7 6 simplbi 
 |-  ( x e. ( Rng i^i U ) -> x e. Rng )
8 5 7 biimtrdi 
 |-  ( ph -> ( x e. B -> x e. Rng ) )
9 8 imp 
 |-  ( ( ph /\ x e. B ) -> x e. Rng )
10 eqid 
 |-  ( Base ` x ) = ( Base ` x )
11 10 idrnghm 
 |-  ( x e. Rng -> ( _I |` ( Base ` x ) ) e. ( x RngHom x ) )
12 9 11 syl 
 |-  ( ( ph /\ x e. B ) -> ( _I |` ( Base ` x ) ) e. ( x RngHom x ) )
13 eqid 
 |-  ( Id ` C ) = ( Id ` C )
14 2 adantr 
 |-  ( ( ph /\ x e. B ) -> U e. V )
15 6 simprbi 
 |-  ( x e. ( Rng i^i U ) -> x e. U )
16 5 15 biimtrdi 
 |-  ( ph -> ( x e. B -> x e. U ) )
17 16 imp 
 |-  ( ( ph /\ x e. B ) -> x e. U )
18 1 13 14 17 estrcid 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) = ( _I |` ( Base ` x ) ) )
19 4 oveqdr 
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x ( RngHom |` ( B X. B ) ) x ) )
20 eqid 
 |-  ( RngCat ` U ) = ( RngCat ` U )
21 eqid 
 |-  ( Base ` ( RngCat ` U ) ) = ( Base ` ( RngCat ` U ) )
22 eqid 
 |-  ( Hom ` ( RngCat ` U ) ) = ( Hom ` ( RngCat ` U ) )
23 20 21 2 22 rngchomfval 
 |-  ( ph -> ( Hom ` ( RngCat ` U ) ) = ( RngHom |` ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) ) )
24 20 21 2 rngcbas 
 |-  ( ph -> ( Base ` ( RngCat ` U ) ) = ( U i^i Rng ) )
25 incom 
 |-  ( Rng i^i U ) = ( U i^i Rng )
26 3 25 eqtrdi 
 |-  ( ph -> B = ( U i^i Rng ) )
27 26 eqcomd 
 |-  ( ph -> ( U i^i Rng ) = B )
28 24 27 eqtrd 
 |-  ( ph -> ( Base ` ( RngCat ` U ) ) = B )
29 28 sqxpeqd 
 |-  ( ph -> ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) = ( B X. B ) )
30 29 reseq2d 
 |-  ( ph -> ( RngHom |` ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) ) = ( RngHom |` ( B X. B ) ) )
31 23 30 eqtrd 
 |-  ( ph -> ( Hom ` ( RngCat ` U ) ) = ( RngHom |` ( B X. B ) ) )
32 31 adantr 
 |-  ( ( ph /\ x e. B ) -> ( Hom ` ( RngCat ` U ) ) = ( RngHom |` ( B X. B ) ) )
33 32 eqcomd 
 |-  ( ( ph /\ x e. B ) -> ( RngHom |` ( B X. B ) ) = ( Hom ` ( RngCat ` U ) ) )
34 33 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x ( RngHom |` ( B X. B ) ) x ) = ( x ( Hom ` ( RngCat ` U ) ) x ) )
35 26 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( U i^i Rng ) ) )
36 35 biimpa 
 |-  ( ( ph /\ x e. B ) -> x e. ( U i^i Rng ) )
37 24 adantr 
 |-  ( ( ph /\ x e. B ) -> ( Base ` ( RngCat ` U ) ) = ( U i^i Rng ) )
38 36 37 eleqtrrd 
 |-  ( ( ph /\ x e. B ) -> x e. ( Base ` ( RngCat ` U ) ) )
39 20 21 14 22 38 38 rngchom 
 |-  ( ( ph /\ x e. B ) -> ( x ( Hom ` ( RngCat ` U ) ) x ) = ( x RngHom x ) )
40 19 34 39 3eqtrd 
 |-  ( ( ph /\ x e. B ) -> ( x H x ) = ( x RngHom x ) )
41 12 18 40 3eltr4d 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )