Metamath Proof Explorer


Theorem suppofss1d

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

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

Proof

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 𝑍 ) )