Step |
Hyp |
Ref |
Expression |
1 |
|
suppofssd.1 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
suppofssd.2 |
⊢ ( 𝜑 → 𝑍 ∈ 𝐵 ) |
3 |
|
suppofssd.3 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
4 |
|
suppofssd.4 |
⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 ) |
5 |
|
suppofss1d.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑍 𝑋 𝑥 ) = 𝑍 ) |
6 |
3
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) |
7 |
4
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn 𝐴 ) |
8 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
9 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
10 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
11 |
6 7 1 1 8 9 10
|
ofval |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) 𝑋 ( 𝐺 ‘ 𝑦 ) ) ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) 𝑋 ( 𝐺 ‘ 𝑦 ) ) ) |
13 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) |
14 |
13
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑋 ( 𝐺 ‘ 𝑦 ) ) = ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) ) |
15 |
5
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑍 𝑋 𝑥 ) = 𝑍 ) |
16 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑍 𝑋 𝑥 ) = 𝑍 ) |
17 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 ) |
18 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ( 𝐺 ‘ 𝑦 ) ) → 𝑥 = ( 𝐺 ‘ 𝑦 ) ) |
19 |
18
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ( 𝐺 ‘ 𝑦 ) ) → ( 𝑍 𝑋 𝑥 ) = ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) ) |
20 |
19
|
eqeq1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ( 𝐺 ‘ 𝑦 ) ) → ( ( 𝑍 𝑋 𝑥 ) = 𝑍 ↔ ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) = 𝑍 ) ) |
21 |
17 20
|
rspcdv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑍 𝑋 𝑥 ) = 𝑍 → ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) = 𝑍 ) ) |
22 |
16 21
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) = 𝑍 ) |
23 |
22
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) → ( 𝑍 𝑋 ( 𝐺 ‘ 𝑦 ) ) = 𝑍 ) |
24 |
12 14 23
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) |
25 |
24
|
ex |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑍 → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) ) |
26 |
25
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = 𝑍 → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) ) |
27 |
6 7 1 1 8
|
offn |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑋 𝐺 ) Fn 𝐴 ) |
28 |
|
ssidd |
⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 ) |
29 |
|
suppfnss |
⊢ ( ( ( ( 𝐹 ∘f 𝑋 𝐺 ) Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = 𝑍 → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) |
30 |
27 6 28 1 2 29
|
syl23anc |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = 𝑍 → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) |
31 |
26 30
|
mpd |
⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) |