Metamath Proof Explorer

Theorem isvclem

Description: Lemma for isvcOLD . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypothesis isvclem.1 ⊢ X = ran ⁡ G
Assertion isvclem ⊢ G ∈ V ∧ S ∈ V → G S ∈ CVec OLD ↔ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x

Proof

Step Hyp Ref Expression
1 isvclem.1 ⊢ X = ran ⁡ G
2 df-vc ⊢ CVec OLD = g s | g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x
3 2 eleq2i ⊢ G S ∈ CVec OLD ↔ G S ∈ g s | g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x
4 eleq1 ⊢ g = G → g ∈ AbelOp ↔ G ∈ AbelOp
5 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
6 5 1 eqtr4di ⊢ g = G → ran ⁡ g = X
7 xpeq2 ⊢ ran ⁡ g = X → ℂ × ran ⁡ g = ℂ × X
8 7 feq2d ⊢ ran ⁡ g = X → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ ran ⁡ g
9 feq3 ⊢ ran ⁡ g = X → s : ℂ × X ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
10 8 9 bitrd ⊢ ran ⁡ g = X → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
11 6 10 syl ⊢ g = G → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
12 oveq ⊢ g = G → x g z = x G z
13 12 oveq2d ⊢ g = G → y s x g z = y s x G z
14 oveq ⊢ g = G → y s x g y s z = y s x G y s z
15 13 14 eqeq12d ⊢ g = G → y s x g z = y s x g y s z ↔ y s x G z = y s x G y s z
16 6 15 raleqbidv ⊢ g = G → ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ↔ ∀ z ∈ X y s x G z = y s x G y s z
17 oveq ⊢ g = G → y s x g z s x = y s x G z s x
18 17 eqeq2d ⊢ g = G → y + z s x = y s x g z s x ↔ y + z s x = y s x G z s x
19 18 anbi1d ⊢ g = G → y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
20 19 ralbidv ⊢ g = G → ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
21 16 20 anbi12d ⊢ g = G → ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
22 21 ralbidv ⊢ g = G → ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
23 22 anbi2d ⊢ g = G → 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
24 6 23 raleqbidv ⊢ g = G → ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ x ∈ X 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
25 4 11 24 3anbi123d ⊢ g = G → g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ G ∈ AbelOp ∧ s : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
26 feq1 ⊢ s = S → s : ℂ × X ⟶ X ↔ S : ℂ × X ⟶ X
27 oveq ⊢ s = S → 1 s x = 1 S x
28 27 eqeq1d ⊢ s = S → 1 s x = x ↔ 1 S x = x
29 oveq ⊢ s = S → y s x G z = y S x G z
30 oveq ⊢ s = S → y s x = y S x
31 oveq ⊢ s = S → y s z = y S z
32 30 31 oveq12d ⊢ s = S → y s x G y s z = y S x G y S z
33 29 32 eqeq12d ⊢ s = S → y s x G z = y s x G y s z ↔ y S x G z = y S x G y S z
34 33 ralbidv ⊢ s = S → ∀ z ∈ X y s x G z = y s x G y s z ↔ ∀ z ∈ X y S x G z = y S x G y S z
35 oveq ⊢ s = S → y + z s x = y + z S x
36 oveq ⊢ s = S → z s x = z S x
37 30 36 oveq12d ⊢ s = S → y s x G z s x = y S x G z S x
38 35 37 eqeq12d ⊢ s = S → y + z s x = y s x G z s x ↔ y + z S x = y S x G z S x
39 oveq ⊢ s = S → y ⁢ z s x = y ⁢ z S x
40 oveq ⊢ s = S → y s z s x = y S z s x
41 36 oveq2d ⊢ s = S → y S z s x = y S z S x
42 40 41 eqtrd ⊢ s = S → y s z s x = y S z S x
43 39 42 eqeq12d ⊢ s = S → y ⁢ z s x = y s z s x ↔ y ⁢ z S x = y S z S x
44 38 43 anbi12d ⊢ s = S → y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
45 44 ralbidv ⊢ s = S → ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
46 34 45 anbi12d ⊢ s = S → ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
47 46 ralbidv ⊢ s = S → ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
48 28 47 anbi12d ⊢ s = S → 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
49 48 ralbidv ⊢ s = S → ∀ x ∈ X 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
50 26 49 3anbi23d ⊢ s = S → G ∈ AbelOp ∧ s : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y s x G z = y s x G y s z ∧ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
51 25 50 opelopabg ⊢ G ∈ V ∧ S ∈ V → G S ∈ g s | g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ∧ ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
52 3 51 bitrid ⊢ G ∈ V ∧ S ∈ V → G S ∈ CVec OLD ↔ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x