Metamath Proof Explorer

Theorem isores3

Description: Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Assertion isores3 ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = ( 𝐻 “ 𝐾 ) ) → ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 f1of1 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –1-1→ 𝐵 )
2 f1ores ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝐾 ⊆ 𝐴 ) → ( 𝐻 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( 𝐻 “ 𝐾 ) )
3 2 expcom ⊢ ( 𝐾 ⊆ 𝐴 → ( 𝐻 : 𝐴 –1-1→ 𝐵 → ( 𝐻 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( 𝐻 “ 𝐾 ) ) )
4 1 3 syl5 ⊢ ( 𝐾 ⊆ 𝐴 → ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐻 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( 𝐻 “ 𝐾 ) ) )
5 ssralv ⊢ ( 𝐾 ⊆ 𝐴 → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
6 ssralv ⊢ ( 𝐾 ⊆ 𝐴 → ( ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
7 6 adantr ⊢ ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) → ( ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
8 fvres ⊢ ( 𝑎 ∈ 𝐾 → ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
9 fvres ⊢ ( 𝑏 ∈ 𝐾 → ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) = ( 𝐻 ‘ 𝑏 ) )
10 8 9 breqan12d ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
11 10 adantll ⊢ ( ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑏 ∈ 𝐾 ) → ( ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
12 11 bibi2d ⊢ ( ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑏 ∈ 𝐾 ) → ( ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ↔ ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
13 12 biimprd ⊢ ( ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) ∧ 𝑏 ∈ 𝐾 ) → ( ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
14 13 ralimdva ⊢ ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) → ( ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
15 7 14 syld ⊢ ( ( 𝐾 ⊆ 𝐴 ∧ 𝑎 ∈ 𝐾 ) → ( ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
16 15 ralimdva ⊢ ( 𝐾 ⊆ 𝐴 → ( ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
17 5 16 syld ⊢ ( 𝐾 ⊆ 𝐴 → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) → ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
18 4 17 anim12d ⊢ ( 𝐾 ⊆ 𝐴 → ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) → ( ( 𝐻 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( 𝐻 “ 𝐾 ) ∧ ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) ) )
19 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
20 df-isom ⊢ ( ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , ( 𝐻 “ 𝐾 ) ) ↔ ( ( 𝐻 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( 𝐻 “ 𝐾 ) ∧ ∀ 𝑎 ∈ 𝐾 ∀ 𝑏 ∈ 𝐾 ( 𝑎 𝑅 𝑏 ↔ ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑎 ) 𝑆 ( ( 𝐻 ↾ 𝐾 ) ‘ 𝑏 ) ) ) )
21 18 19 20 3imtr4g ⊢ ( 𝐾 ⊆ 𝐴 → ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , ( 𝐻 “ 𝐾 ) ) ) )
22 21 impcom ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐾 ⊆ 𝐴 ) → ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , ( 𝐻 “ 𝐾 ) ) )
23 isoeq5 ⊢ ( 𝑋 = ( 𝐻 “ 𝐾 ) → ( ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , 𝑋 ) ↔ ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , ( 𝐻 “ 𝐾 ) ) ) )
24 22 23 syl5ibrcom ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐾 ⊆ 𝐴 ) → ( 𝑋 = ( 𝐻 “ 𝐾 ) → ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , 𝑋 ) ) )
25 24 3impia ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = ( 𝐻 “ 𝐾 ) ) → ( 𝐻 ↾ 𝐾 ) Isom 𝑅 , 𝑆 ( 𝐾 , 𝑋 ) )