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

Theorem rngohomco 35370
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 2822 . . . . . . 7 (1st𝑆) = (1st𝑆)
2 eqid 2822 . . . . . . 7 ran (1st𝑆) = ran (1st𝑆)
3 eqid 2822 . . . . . . 7 (1st𝑇) = (1st𝑇)
4 eqid 2822 . . . . . . 7 ran (1st𝑇) = ran (1st𝑇)
51, 2, 3, 4rngohomf 35362 . . . . . 6 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
653expa 1115 . . . . 5 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
763adantl1 1163 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
87adantrl 715 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → 𝐺:ran (1st𝑆)⟶ran (1st𝑇))
9 eqid 2822 . . . . . . 7 (1st𝑅) = (1st𝑅)
10 eqid 2822 . . . . . . 7 ran (1st𝑅) = ran (1st𝑅)
119, 10, 1, 2rngohomf 35362 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
12113expa 1115 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
13123adantl3 1165 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
1413adantrr 716 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → 𝐹:ran (1st𝑅)⟶ran (1st𝑆))
15 fco 6512 . . 3 ((𝐺:ran (1st𝑆)⟶ran (1st𝑇) ∧ 𝐹:ran (1st𝑅)⟶ran (1st𝑆)) → (𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇))
168, 14, 15syl2anc 587 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇))
17 eqid 2822 . . . . . . 7 (2nd𝑅) = (2nd𝑅)
18 eqid 2822 . . . . . . 7 (GId‘(2nd𝑅)) = (GId‘(2nd𝑅))
1910, 17, 18rngo1cl 35335 . . . . . 6 (𝑅 ∈ RingOps → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
20193ad2ant1 1130 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
2120adantr 484 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (GId‘(2nd𝑅)) ∈ ran (1st𝑅))
22 fvco3 6742 . . . 4 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (GId‘(2nd𝑅)) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd𝑅)))))
2314, 21, 22syl2anc 587 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd𝑅)))))
24 eqid 2822 . . . . . . . . 9 (2nd𝑆) = (2nd𝑆)
25 eqid 2822 . . . . . . . . 9 (GId‘(2nd𝑆)) = (GId‘(2nd𝑆))
2617, 18, 24, 25rngohom1 35364 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
27263expa 1115 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
28273adantl3 1165 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
2928adantrr 716 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐹‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑆)))
3029fveq2d 6656 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd𝑅)))) = (𝐺‘(GId‘(2nd𝑆))))
31 eqid 2822 . . . . . . . 8 (2nd𝑇) = (2nd𝑇)
32 eqid 2822 . . . . . . . 8 (GId‘(2nd𝑇)) = (GId‘(2nd𝑇))
3324, 25, 31, 32rngohom1 35364 . . . . . . 7 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
34333expa 1115 . . . . . 6 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
35343adantl1 1163 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
3635adantrl 715 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(GId‘(2nd𝑆))) = (GId‘(2nd𝑇)))
3730, 36eqtrd 2857 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd𝑅)))) = (GId‘(2nd𝑇)))
3823, 37eqtrd 2857 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)))
399, 10, 1rngohomadd 35365 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4039ex 416 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
41403expa 1115 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
42413adantl3 1165 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
4342imp 410 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4443adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)(1st𝑆)(𝐹𝑦)))
4544fveq2d 6656 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))) = (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))))
469, 10, 1, 2rngohomcl 35363 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) → (𝐹𝑥) ∈ ran (1st𝑆))
479, 10, 1, 2rngohomcl 35363 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹𝑦) ∈ ran (1st𝑆))
4846, 47anim12dan 621 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
4948ex 416 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
50493expa 1115 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
51503adantl3 1165 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))))
5251imp 410 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
5352adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)))
541, 2, 3rngohomadd 35365 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
5554ex 416 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
56553expa 1115 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
57563adantl1 1163 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦)))))
5857imp 410 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
5958adantlrl 719 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
6053, 59syldan 594 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘((𝐹𝑥)(1st𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
6145, 60eqtrd 2857 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
629, 10rngogcl 35308 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
63623expb 1117 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
64633ad2antl1 1182 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
6564adantlr 714 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
66 fvco3 6742 . . . . . . 7 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
6714, 66sylan 583 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
6865, 67syldan 594 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st𝑅)𝑦))))
69 fvco3 6742 . . . . . . . 8 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ 𝑥 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
7014, 69sylan 583 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ 𝑥 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
71 fvco3 6742 . . . . . . . 8 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦)))
7214, 71sylan 583 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ 𝑦 ∈ ran (1st𝑅)) → ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦)))
7370, 72anim12dan 621 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))))
74 oveq12 7149 . . . . . 6 ((((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))) → (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
7573, 74syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(1st𝑇)(𝐺‘(𝐹𝑦))))
7661, 68, 753eqtr4d 2867 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)))
779, 10, 17, 24rngohommul 35366 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
7877ex 416 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
79783expa 1115 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
80793adantl3 1165 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
8180imp 410 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
8281adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑦)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑦)))
8382fveq2d 6656 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))) = (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))))
841, 2, 24, 31rngohommul 35366 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
8584ex 416 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
86853expa 1115 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
87863adantl1 1163 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) → (((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆)) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦)))))
8887imp 410 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
8988adantlrl 719 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((𝐹𝑥) ∈ ran (1st𝑆) ∧ (𝐹𝑦) ∈ ran (1st𝑆))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
9053, 89syldan 594 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘((𝐹𝑥)(2nd𝑆)(𝐹𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
9183, 90eqtrd 2857 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
929, 17, 10rngocl 35297 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
93923expb 1117 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
94933ad2antl1 1182 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
9594adantlr 714 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅))
96 fvco3 6742 . . . . . . 7 ((𝐹:ran (1st𝑅)⟶ran (1st𝑆) ∧ (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
9714, 96sylan 583 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥(2nd𝑅)𝑦) ∈ ran (1st𝑅)) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
9895, 97syldan 594 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd𝑅)𝑦))))
99 oveq12 7149 . . . . . 6 ((((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)) ∧ ((𝐺𝐹)‘𝑦) = (𝐺‘(𝐹𝑦))) → (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
10073, 99syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)) = ((𝐺‘(𝐹𝑥))(2nd𝑇)(𝐺‘(𝐹𝑦))))
10191, 98, 1003eqtr4d 2867 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦)))
10276, 101jca 515 . . 3 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))
103102ralrimivva 3181 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 35361 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇) ∧ ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))))
1051043adant2 1128 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺𝐹):ran (1st𝑅)⟶ran (1st𝑇) ∧ ((𝐺𝐹)‘(GId‘(2nd𝑅))) = (GId‘(2nd𝑇)) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(((𝐺𝐹)‘(𝑥(1st𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(1st𝑇)((𝐺𝐹)‘𝑦)) ∧ ((𝐺𝐹)‘(𝑥(2nd𝑅)𝑦)) = (((𝐺𝐹)‘𝑥)(2nd𝑇)((𝐺𝐹)‘𝑦))))))
106105adantr 484 . 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 1339 1 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) → (𝐺𝐹) ∈ (𝑅 RngHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wral 3130  ran crn 5533  ccom 5536  wf 6330  cfv 6334  (class class class)co 7140  1st c1st 7673  2nd c2nd 7674  GIdcgi 28271  RingOpscrngo 35290   RngHom crnghom 35356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fo 6340  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-1st 7675  df-2nd 7676  df-map 8395  df-grpo 28274  df-gid 28275  df-ablo 28326  df-ass 35239  df-exid 35241  df-mgmOLD 35245  df-sgrOLD 35257  df-mndo 35263  df-rngo 35291  df-rngohom 35359
This theorem is referenced by:  rngoisoco  35378
  Copyright terms: Public domain W3C validator