 Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngohomco Structured version   Visualization version   GIF version

Theorem rngohomco 34082
 Description: The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
rngohomco (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺𝐹) ∈ (𝑅 RngHom 𝑇))

Proof of Theorem rngohomco
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2756 . . . . . . 7 (1st𝑆) = (1st𝑆)
2 eqid 2756 . . . . . . 7 ran (1st𝑆) = ran (1st𝑆)
3 eqid 2756 . . . . . . 7 (1st𝑇) = (1st𝑇)
4 eqid 2756 . . . . . . 7 ran (1st𝑇) = ran (1st𝑇)
51, 2, 3, 4rngohomf 34074 . . . . . 6 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
653expa 1112 . . . . 5 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
763adantl1 1172 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
87adantrl 754 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
9 eqid 2756 . . . . . . 7 (1st𝑅) = (1st𝑅)
10 eqid 2756 . . . . . . 7 ran (1st𝑅) = ran (1st𝑅)
119, 10, 1, 2rngohomf 34074 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
12113expa 1112 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
13123adantl3 1174 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
1413adantrr 755 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
15 fco 6215 . . 3 ((𝐺:ran (1st𝑆)⟶ran (1st𝑇) ∧ 𝐹:ran (1st𝑅)⟶ran (1st𝑆)) → (𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇))
168, 14, 15syl2anc 696 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇))
17 eqid 2756 . . . . . . 7 (2nd𝑅) = (2nd𝑅)
18 eqid 2756 . . . . . . 7 (GId‘(2nd𝑅)) = (GId‘(2nd𝑅))
1910, 17, 18rngo1cl 34047 . . . . . 6 (𝑅 ∈ RingOps → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
20193ad2ant1 1128 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
2120adantr 472 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
22 fvco3 6433 . . . 4 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (GId‘(2nd𝑅)) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd𝑅)))))
2314, 21, 22syl2anc 696 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd𝑅)))))
24 eqid 2756 . . . . . . . . 9 (2nd𝑆) = (2nd𝑆)
25 eqid 2756 . . . . . . . . 9 (GId‘(2nd𝑆)) = (GId‘(2nd𝑆))
2617, 18, 24, 25rngohom1 34076 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
27263expa 1112 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
28273adantl3 1174 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
2928adantrr 755 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
3029fveq2d 6352 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd𝑅)))) = (𝐺‘(GId‘(2nd𝑆))))
31 eqid 2756 . . . . . . . 8 (2nd𝑇) = (2nd𝑇)
32 eqid 2756 . . . . . . . 8 (GId‘(2nd𝑇)) = (GId‘(2nd𝑇))
3324, 25, 31, 32rngohom1 34076 . . . . . . 7 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
34333expa 1112 . . . . . 6 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
35343adantl1 1172 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
3635adantrl 754 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
3730, 36eqtrd 2790 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd𝑅)))) = (GId‘(2nd𝑇)))
3823, 37eqtrd 2790 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)))
399, 10, 1rngohomadd 34077 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4039ex 449 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
41403expa 1112 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
42413adantl3 1174 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
4342imp 444 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4443adantlrr 759 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4544fveq2d 6352 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))) = (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
469, 10, 1, 2rngohomcl 34075 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) → (𝐹𝑥) ∈ ran (1st𝑆))
479, 10, 1, 2rngohomcl 34075 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹𝑦) ∈ ran (1st𝑆))
4846, 47anim12da 33815 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
4948ex 449 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
50493expa 1112 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
51503adantl3 1174 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
5251imp 444 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
5352adantlrr 759 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
541, 2, 3rngohomadd 34077 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
5554ex 449 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
56553expa 1112 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
57563adantl1 1172 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
5857imp 444 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
5958adantlrl 758 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
6053, 59syldan 488 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
6145, 60eqtrd 2790 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
629, 10rngogcl 34020 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
63623expb 1114 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
64633ad2antl1 1201 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
6564adantlr 753 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
66 fvco3 6433 . . . . . . 7 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
6714, 66sylan 489 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
6865, 67syldan 488 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
69 fvco3 6433 . . . . . . . 8 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ 𝑥 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
7014, 69sylan 489 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ 𝑥 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
71 fvco3 6433 . . . . . . . 8 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦)))
7214, 71sylan 489 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦)))
7370, 72anim12da 33815 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))))
74 oveq12 6818 . . . . . 6 ((((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))) → (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
7573, 74syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
7661, 68, 753eqtr4d 2800 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)))
779, 10, 17, 24rngohommul 34078 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
7877ex 449 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
79783expa 1112 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
80793adantl3 1174 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
8180imp 444 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
8281adantlrr 759 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
8382fveq2d 6352 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))) = (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
841, 2, 24, 31rngohommul 34078 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
8584ex 449 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
86853expa 1112 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
87863adantl1 1172 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
8887imp 444 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
8988adantlrl 758 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
9053, 89syldan 488 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
9183, 90eqtrd 2790 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
929, 17, 10rngocl 34009 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
93923expb 1114 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
94933ad2antl1 1201 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
9594adantlr 753 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
96 fvco3 6433 . . . . . . 7 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
9714, 96sylan 489 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
9895, 97syldan 488 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
99 oveq12 6818 . . . . . 6 ((((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))) → (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
10073, 99syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
10191, 98, 1003eqtr4d 2800 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)))
10276, 101jca 555 . . 3 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))
103102ralrimivva 3105 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 34073 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇) ∧ ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))))
1051043adant2 1126 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇) ∧ ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))))
106105adantr 472 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ((𝐺𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇) ∧ ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))))
10716, 38, 103, 106mpbir3and 1428 1 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺𝐹) ∈ (𝑅 RngHom 𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1628   ∈ wcel 2135  ∀wral 3046  ran crn 5263   ∘ ccom 5266  ⟶wf 6041  ‘cfv 6045  (class class class)co 6809  1st c1st 7327  2nd c2nd 7328  GIdcgi 27649  RingOpscrngo 34002   RngHom crnghom 34068 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-fo 6051  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-1st 7329  df-2nd 7330  df-map 8021  df-grpo 27652  df-gid 27653  df-ablo 27704  df-ass 33951  df-exid 33953  df-mgmOLD 33957  df-sgrOLD 33969  df-mndo 33975  df-rngo 34003  df-rngohom 34071 This theorem is referenced by:  rngoisoco  34090
 Copyright terms: Public domain W3C validator