Metamath Proof Explorer

Theorem grtrimap

Description: Conditions for mapping triangles onto triangles. Lemma for grimgrtri and grlimgrtri . (Contributed by AV, 23-Aug-2025)

Ref Expression
Assertion grtrimap ⊢ F : V ⟶ 1-1 W → a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3

Proof

Step Hyp Ref Expression
1 f1f ⊢ F : V ⟶ 1-1 W → F : V ⟶ W
2 1 ffvelcdmda ⊢ F : V ⟶ 1-1 W ∧ a ∈ V → F ⁡ a ∈ W
3 2 ex ⊢ F : V ⟶ 1-1 W → a ∈ V → F ⁡ a ∈ W
4 1 ffvelcdmda ⊢ F : V ⟶ 1-1 W ∧ b ∈ V → F ⁡ b ∈ W
5 4 ex ⊢ F : V ⟶ 1-1 W → b ∈ V → F ⁡ b ∈ W
6 1 ffvelcdmda ⊢ F : V ⟶ 1-1 W ∧ c ∈ V → F ⁡ c ∈ W
7 6 ex ⊢ F : V ⟶ 1-1 W → c ∈ V → F ⁡ c ∈ W
8 3 5 7 3anim123d ⊢ F : V ⟶ 1-1 W → a ∈ V ∧ b ∈ V ∧ c ∈ V → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W
9 8 adantrd ⊢ F : V ⟶ 1-1 W → a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W
10 9 imp ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W
11 imaeq2 ⊢ T = a b c → F T = F a b c
12 11 ad2antrl ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F T = F a b c
13 12 adantl ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F T = F a b c
14 f1fn ⊢ F : V ⟶ 1-1 W → F Fn V
15 14 adantr ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F Fn V
16 simprl1 ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → a ∈ V
17 simprl2 ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → b ∈ V
18 simprl3 ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → c ∈ V
19 15 16 17 18 fnimatpd ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F a b c = F ⁡ a F ⁡ b F ⁡ c
20 13 19 eqtrd ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F T = F ⁡ a F ⁡ b F ⁡ c
21 simpl ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F : V ⟶ 1-1 W
22 tpssi ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V → a b c ⊆ V
23 22 adantr ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → a b c ⊆ V
24 sseq1 ⊢ T = a b c → T ⊆ V ↔ a b c ⊆ V
25 24 ad2antrl ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T ⊆ V ↔ a b c ⊆ V
26 23 25 mpbird ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T ⊆ V
27 26 adantl ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T ⊆ V
28 tpex ⊢ a b c ∈ V
29 eleq1 ⊢ T = a b c → T ∈ V ↔ a b c ∈ V
30 28 29 mpbiri ⊢ T = a b c → T ∈ V
31 30 ad2antrl ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T ∈ V
32 31 adantl ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T ∈ V
33 f1imaeng ⊢ F : V ⟶ 1-1 W ∧ T ⊆ V ∧ T ∈ V → F T ≈ T
34 hasheni ⊢ F T ≈ T → F T = T
35 33 34 syl ⊢ F : V ⟶ 1-1 W ∧ T ⊆ V ∧ T ∈ V → F T = T
36 35 eqcomd ⊢ F : V ⟶ 1-1 W ∧ T ⊆ V ∧ T ∈ V → T = F T
37 21 27 32 36 syl3anc ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T = F T
38 simprrr ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → T = 3
39 37 38 eqtr3d ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F T = 3
40 10 20 39 3jca ⊢ F : V ⟶ 1-1 W ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3
41 40 ex ⊢ F : V ⟶ 1-1 W → a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ W ∧ F ⁡ b ∈ W ∧ F ⁡ c ∈ W ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3