Metamath Proof Explorer

Theorem rhmsubcALTVlem4

Description: Lemma 4 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

Ref Expression
Hypotheses rngcrescrhmALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhmALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcrescrhmALTV.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhmALTV.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubcALTVlem4 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhmALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
3 rngcrescrhmALTV.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhmALTV.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝜑 )
6 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝜑 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝑅 )
8 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
9 simpl ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑦 ∈ 𝑅 )
10 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
11 1 2 3 4 rhmsubcALTVlem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
12 6 8 10 11 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
13 12 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) )
14 simpr ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ 𝑅 )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑅 )
16 1 2 3 4 rhmsubcALTVlem2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
17 6 10 15 16 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
18 17 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) )
19 13 18 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ↔ ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) ) )
20 rhmco ⊢ ( ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ∧ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
21 20 ancoms ⊢ ( ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
22 19 21 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) ) )
23 22 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
24 eqid ⊢ ( RngCatALTV ‘ 𝑈 ) = ( RngCatALTV ‘ 𝑈 )
25 eqid ⊢ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( Base ‘ ( RngCatALTV ‘ 𝑈 ) )
26 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑈 ∈ 𝑉 )
27 eqid ⊢ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( comp ‘ ( RngCatALTV ‘ 𝑈 ) )
28 incom ⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
29 ringrng ⊢ ( 𝑥 ∈ Ring → 𝑥 ∈ Rng )
30 29 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ Ring → 𝑥 ∈ Rng ) )
31 30 ssrdv ⊢ ( 𝜑 → Ring ⊆ Rng )
32 sslin ⊢ ( Ring ⊆ Rng → ( 𝑈 ∩ Ring ) ⊆ ( 𝑈 ∩ Rng ) )
33 31 32 syl ⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ⊆ ( 𝑈 ∩ Rng ) )
34 28 33 eqsstrid ⊢ ( 𝜑 → ( Ring ∩ 𝑈 ) ⊆ ( 𝑈 ∩ Rng ) )
35 24 25 1 rngcbasALTV ⊢ ( 𝜑 → ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑈 ∩ Rng ) )
36 34 3 35 3sstr4d ⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
37 36 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
39 38 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
40 36 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑅 → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑦 ∈ 𝑅 → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
42 41 com12 ⊢ ( 𝑦 ∈ 𝑅 → ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
43 42 adantr ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
44 43 impcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
45 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
46 36 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
48 47 adantld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ) )
49 48 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
50 49 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
51 rhmisrnghm ⊢ ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) → 𝑓 ∈ ( 𝑥 RngHom 𝑦 ) )
52 13 51 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 ∈ ( 𝑥 RngHom 𝑦 ) ) )
53 52 com12 ⊢ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑓 ∈ ( 𝑥 RngHom 𝑦 ) ) )
54 53 adantr ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑓 ∈ ( 𝑥 RngHom 𝑦 ) ) )
55 54 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 RngHom 𝑦 ) )
56 rhmisrnghm ⊢ ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) → 𝑔 ∈ ( 𝑦 RngHom 𝑧 ) )
57 18 56 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → 𝑔 ∈ ( 𝑦 RngHom 𝑧 ) ) )
58 57 adantld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 ∈ ( 𝑦 RngHom 𝑧 ) ) )
59 58 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 RngHom 𝑧 ) )
60 24 25 26 27 39 45 50 55 59 rngccoALTV ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
61 1 2 3 4 rhmsubcALTVlem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
62 6 8 15 61 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
63 62 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
64 23 60 63 3eltr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCatALTV ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )