Metamath Proof Explorer

Theorem suppofss2d

Description: Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses suppofssd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppofssd.2 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
suppofssd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
suppofssd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
suppofss2d.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝑋 𝑍 ) = 𝑍 )
Assertion suppofss2d ( 𝜑 → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 suppofssd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 suppofssd.2 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
3 suppofssd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4 suppofssd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
5 suppofss2d.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 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑋 ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑦 ) 𝑋 𝑍 ) )
15 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 𝑋 𝑍 ) = 𝑍 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 𝑋 𝑍 ) = 𝑍 )
17 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = ( 𝐹 ‘ 𝑦 ) )
19 18 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 𝑋 𝑍 ) = ( ( 𝐹 ‘ 𝑦 ) 𝑋 𝑍 ) )
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 7 28 1 2 29 syl23anc ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑦 ) = 𝑍 ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )
31 26 30 mpd ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )