Metamath Proof Explorer

Theorem resv1r

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

Ref Expression
Hypotheses resvbas.1 ⊢ H = G ↾ 𝑣 A
resv1r.2 ⊢ 1 ˙ = 1 G
Assertion resv1r ⊢ A ∈ V → 1 ˙ = 1 H

Proof

Step Hyp Ref Expression
1 resvbas.1 ⊢ H = G ↾ 𝑣 A
2 resv1r.2 ⊢ 1 ˙ = 1 G
3 eqid ⊢ Base G = Base G
4 1 3 resvbas ⊢ A ∈ V → Base G = Base H
5 4 eleq2d ⊢ A ∈ V → e ∈ Base G ↔ e ∈ Base H
6 eqid ⊢ ⋅ G = ⋅ G
7 1 6 resvmulr ⊢ A ∈ V → ⋅ G = ⋅ H
8 7 oveqd ⊢ A ∈ V → e ⋅ G x = e ⋅ H x
9 8 eqeq1d ⊢ A ∈ V → e ⋅ G x = x ↔ e ⋅ H x = x
10 7 oveqd ⊢ A ∈ V → x ⋅ G e = x ⋅ H e
11 10 eqeq1d ⊢ A ∈ V → x ⋅ G e = x ↔ x ⋅ H e = x
12 9 11 anbi12d ⊢ A ∈ V → e ⋅ G x = x ∧ x ⋅ G e = x ↔ e ⋅ H x = x ∧ x ⋅ H e = x
13 4 12 raleqbidv ⊢ A ∈ V → ∀ x ∈ Base G e ⋅ G x = x ∧ x ⋅ G e = x ↔ ∀ x ∈ Base H e ⋅ H x = x ∧ x ⋅ H e = x
14 5 13 anbi12d ⊢ A ∈ V → e ∈ Base G ∧ ∀ x ∈ Base G e ⋅ G x = x ∧ x ⋅ G e = x ↔ e ∈ Base H ∧ ∀ x ∈ Base H e ⋅ H x = x ∧ x ⋅ H e = x
15 14 iotabidv ⊢ A ∈ V → ι e | e ∈ Base G ∧ ∀ x ∈ Base G e ⋅ G x = x ∧ x ⋅ G e = x = ι e | e ∈ Base H ∧ ∀ x ∈ Base H e ⋅ H x = x ∧ x ⋅ H e = x
16 3 6 2 dfur2 ⊢ 1 ˙ = ι e | e ∈ Base G ∧ ∀ x ∈ Base G e ⋅ G x = x ∧ x ⋅ G e = x
17 eqid ⊢ Base H = Base H
18 eqid ⊢ ⋅ H = ⋅ H
19 eqid ⊢ 1 H = 1 H
20 17 18 19 dfur2 ⊢ 1 H = ι e | e ∈ Base H ∧ ∀ x ∈ Base H e ⋅ H x = x ∧ x ⋅ H e = x
21 15 16 20 3eqtr4g ⊢ A ∈ V → 1 ˙ = 1 H