Metamath Proof Explorer

Theorem resv1r

Description: 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses resvbas.1 ⊢ 𝐻 = ( 𝐺 ↾v 𝐴 )
resv1r.2 ⊢ 1 = ( 1r ‘ 𝐺 )
Assertion resv1r ( 𝐴 ∈ 𝑉 → 1 = ( 1r ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 ⊢ 𝐻 = ( 𝐺 ↾v 𝐴 )
2 resv1r.2 ⊢ 1 = ( 1r ‘ 𝐺 )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 1 3 resvbas ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5 4 eleq2d ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑒 ∈ ( Base ‘ 𝐺 ) ↔ 𝑒 ∈ ( Base ‘ 𝐻 ) ) )
6 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
7 1 6 resvmulr ⊢ ( 𝐴 ∈ 𝑉 → ( .r ‘ 𝐺 ) = ( .r ‘ 𝐻 ) )
8 7 oveqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ↔ ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ) )
10 7 oveqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) )
11 10 eqeq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ↔ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) )
12 9 11 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) ) )
13 4 12 raleqbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) ) )
14 5 13 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑒 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) ) ) )
15 14 iotabidv ⊢ ( 𝐴 ∈ 𝑉 → ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) ) ) )
16 3 6 2 dfur2 ⊢ 1 = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑒 ( .r ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
17 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
18 eqid ⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 )
19 eqid ⊢ ( 1r ‘ 𝐻 ) = ( 1r ‘ 𝐻 )
20 17 18 19 dfur2 ⊢ ( 1r ‘ 𝐻 ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ( ( 𝑒 ( .r ‘ 𝐻 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐻 ) 𝑒 ) = 𝑥 ) ) )
21 15 16 20 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → 1 = ( 1r ‘ 𝐻 ) )