Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ofco2 Structured version   Visualization version   GIF version

Theorem ofco2 20480
 Description: Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018.)
Assertion
Ref Expression
ofco2 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)))

Proof of Theorem ofco2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr1 1234 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → Fun 𝐻)
2 fvimacnvi 6496 . . . 4 ((Fun 𝐻𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) → (𝐻𝑥) ∈ (dom 𝐹 ∩ dom 𝐺))
31, 2sylan 489 . . 3 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) → (𝐻𝑥) ∈ (dom 𝐹 ∩ dom 𝐺))
4 funfn 6080 . . . . . . 7 (Fun 𝐻𝐻 Fn dom 𝐻)
51, 4sylib 208 . . . . . 6 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → 𝐻 Fn dom 𝐻)
6 dffn5 6405 . . . . . 6 (𝐻 Fn dom 𝐻𝐻 = (𝑥 ∈ dom 𝐻 ↦ (𝐻𝑥)))
75, 6sylib 208 . . . . 5 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → 𝐻 = (𝑥 ∈ dom 𝐻 ↦ (𝐻𝑥)))
87reseq1d 5551 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) = ((𝑥 ∈ dom 𝐻 ↦ (𝐻𝑥)) ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))))
9 cnvimass 5644 . . . . 5 (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ⊆ dom 𝐻
10 resmpt 5608 . . . . 5 ((𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ⊆ dom 𝐻 → ((𝑥 ∈ dom 𝐻 ↦ (𝐻𝑥)) ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ (𝐻𝑥)))
119, 10ax-mp 5 . . . 4 ((𝑥 ∈ dom 𝐻 ↦ (𝐻𝑥)) ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ (𝐻𝑥))
128, 11syl6eq 2811 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ (𝐻𝑥)))
13 offval3 7329 . . . 4 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹𝑓 𝑅𝐺) = (𝑦 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑦)𝑅(𝐺𝑦))))
1413adantr 472 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐹𝑓 𝑅𝐺) = (𝑦 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑦)𝑅(𝐺𝑦))))
15 fveq2 6354 . . . 4 (𝑦 = (𝐻𝑥) → (𝐹𝑦) = (𝐹‘(𝐻𝑥)))
16 fveq2 6354 . . . 4 (𝑦 = (𝐻𝑥) → (𝐺𝑦) = (𝐺‘(𝐻𝑥)))
1715, 16oveq12d 6833 . . 3 (𝑦 = (𝐻𝑥) → ((𝐹𝑦)𝑅(𝐺𝑦)) = ((𝐹‘(𝐻𝑥))𝑅(𝐺‘(𝐻𝑥))))
183, 12, 14, 17fmptco 6561 . 2 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)))) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ ((𝐹‘(𝐻𝑥))𝑅(𝐺‘(𝐻𝑥)))))
19 ovex 6843 . . . . . . . 8 ((𝐹𝑥)𝑅(𝐺𝑥)) ∈ V
2019rgenw 3063 . . . . . . 7 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝐹𝑥)𝑅(𝐺𝑥)) ∈ V
21 eqid 2761 . . . . . . . 8 (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))
2221fnmpt 6182 . . . . . . 7 (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝐹𝑥)𝑅(𝐺𝑥)) ∈ V → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) Fn (dom 𝐹 ∩ dom 𝐺))
2320, 22mp1i 13 . . . . . 6 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) Fn (dom 𝐹 ∩ dom 𝐺))
24 offval3 7329 . . . . . . . 8 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
2524adantr 472 . . . . . . 7 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
2625fneq1d 6143 . . . . . 6 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) Fn (dom 𝐹 ∩ dom 𝐺) ↔ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) Fn (dom 𝐹 ∩ dom 𝐺)))
2723, 26mpbird 247 . . . . 5 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐹𝑓 𝑅𝐺) Fn (dom 𝐹 ∩ dom 𝐺))
28 fndm 6152 . . . . 5 ((𝐹𝑓 𝑅𝐺) Fn (dom 𝐹 ∩ dom 𝐺) → dom (𝐹𝑓 𝑅𝐺) = (dom 𝐹 ∩ dom 𝐺))
2927, 28syl 17 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → dom (𝐹𝑓 𝑅𝐺) = (dom 𝐹 ∩ dom 𝐺))
30 eqimss 3799 . . . 4 (dom (𝐹𝑓 𝑅𝐺) = (dom 𝐹 ∩ dom 𝐺) → dom (𝐹𝑓 𝑅𝐺) ⊆ (dom 𝐹 ∩ dom 𝐺))
31 cores2 5810 . . . 4 (dom (𝐹𝑓 𝑅𝐺) ⊆ (dom 𝐹 ∩ dom 𝐺) → ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (dom 𝐹 ∩ dom 𝐺))) = ((𝐹𝑓 𝑅𝐺) ∘ 𝐻))
3229, 30, 313syl 18 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (dom 𝐹 ∩ dom 𝐺))) = ((𝐹𝑓 𝑅𝐺) ∘ 𝐻))
33 funcnvres2 6131 . . . . 5 (Fun 𝐻(𝐻 ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))))
341, 33syl 17 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐻 ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺))))
3534coeq2d 5441 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (dom 𝐹 ∩ dom 𝐺))) = ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)))))
3632, 35eqtr3d 2797 . 2 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹𝑓 𝑅𝐺) ∘ (𝐻 ↾ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)))))
37 simpr2 1236 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐹𝐻) ∈ V)
38 simpr3 1238 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐺𝐻) ∈ V)
39 offval3 7329 . . . 4 (((𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V) → ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)) = (𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ↦ (((𝐹𝐻)‘𝑥)𝑅((𝐺𝐻)‘𝑥))))
4037, 38, 39syl2anc 696 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)) = (𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ↦ (((𝐹𝐻)‘𝑥)𝑅((𝐺𝐻)‘𝑥))))
41 inpreima 6507 . . . . . 6 (Fun 𝐻 → (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) = ((𝐻 “ dom 𝐹) ∩ (𝐻 “ dom 𝐺)))
421, 41syl 17 . . . . 5 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) = ((𝐻 “ dom 𝐹) ∩ (𝐻 “ dom 𝐺)))
43 dmco 5805 . . . . . 6 dom (𝐹𝐻) = (𝐻 “ dom 𝐹)
44 dmco 5805 . . . . . 6 dom (𝐺𝐻) = (𝐻 “ dom 𝐺)
4543, 44ineq12i 3956 . . . . 5 (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) = ((𝐻 “ dom 𝐹) ∩ (𝐻 “ dom 𝐺))
4642, 45syl6reqr 2814 . . . 4 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) = (𝐻 “ (dom 𝐹 ∩ dom 𝐺)))
47 simplr1 1261 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → Fun 𝐻)
48 inss2 3978 . . . . . . . . 9 (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom (𝐺𝐻)
49 dmcoss 5541 . . . . . . . . 9 dom (𝐺𝐻) ⊆ dom 𝐻
5048, 49sstri 3754 . . . . . . . 8 (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom 𝐻
5150a1i 11 . . . . . . 7 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom 𝐻)
5251sselda 3745 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → 𝑥 ∈ dom 𝐻)
53 fvco 6438 . . . . . 6 ((Fun 𝐻𝑥 ∈ dom 𝐻) → ((𝐹𝐻)‘𝑥) = (𝐹‘(𝐻𝑥)))
5447, 52, 53syl2anc 696 . . . . 5 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → ((𝐹𝐻)‘𝑥) = (𝐹‘(𝐻𝑥)))
55 inss1 3977 . . . . . . . . 9 (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom (𝐹𝐻)
56 dmcoss 5541 . . . . . . . . 9 dom (𝐹𝐻) ⊆ dom 𝐻
5755, 56sstri 3754 . . . . . . . 8 (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom 𝐻
5857a1i 11 . . . . . . 7 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ⊆ dom 𝐻)
5958sselda 3745 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → 𝑥 ∈ dom 𝐻)
60 fvco 6438 . . . . . 6 ((Fun 𝐻𝑥 ∈ dom 𝐻) → ((𝐺𝐻)‘𝑥) = (𝐺‘(𝐻𝑥)))
6147, 59, 60syl2anc 696 . . . . 5 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → ((𝐺𝐻)‘𝑥) = (𝐺‘(𝐻𝑥)))
6254, 61oveq12d 6833 . . . 4 ((((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) ∧ 𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻))) → (((𝐹𝐻)‘𝑥)𝑅((𝐺𝐻)‘𝑥)) = ((𝐹‘(𝐻𝑥))𝑅(𝐺‘(𝐻𝑥))))
6346, 62mpteq12dva 4885 . . 3 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → (𝑥 ∈ (dom (𝐹𝐻) ∩ dom (𝐺𝐻)) ↦ (((𝐹𝐻)‘𝑥)𝑅((𝐺𝐻)‘𝑥))) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ ((𝐹‘(𝐻𝑥))𝑅(𝐺‘(𝐻𝑥)))))
6440, 63eqtrd 2795 . 2 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)) = (𝑥 ∈ (𝐻 “ (dom 𝐹 ∩ dom 𝐺)) ↦ ((𝐹‘(𝐻𝑥))𝑅(𝐺‘(𝐻𝑥)))))
6518, 36, 643eqtr4d 2805 1 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹𝐻) ∈ V ∧ (𝐺𝐻) ∈ V)) → ((𝐹𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2140  ∀wral 3051  Vcvv 3341   ∩ cin 3715   ⊆ wss 3716   ↦ cmpt 4882  ◡ccnv 5266  dom cdm 5267   ↾ cres 5269   “ cima 5270   ∘ ccom 5271  Fun wfun 6044   Fn wfn 6045  ‘cfv 6050  (class class class)co 6815   ∘𝑓 cof 7062 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-of 7064 This theorem is referenced by:  oftpos  20481
 Copyright terms: Public domain W3C validator