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→GS∈CVecOLD↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx

Proof

Step Hyp Ref Expression
1 isvclem.1 ⊢X=ran⁡G
2 df-vc ⊢CVecOLD=gs|g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx
3 2 eleq2i ⊢GS∈CVecOLD↔GS∈gs|g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx
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→xgz=xGz
13 12 oveq2d ⊢g=G→ysxgz=ysxGz
14 oveq ⊢g=G→ysxgysz=ysxGysz
15 13 14 eqeq12d ⊢g=G→ysxgz=ysxgysz↔ysxGz=ysxGysz
16 6 15 raleqbidv ⊢g=G→∀z∈ran⁡gysxgz=ysxgysz↔∀z∈XysxGz=ysxGysz
17 oveq ⊢g=G→ysxgzsx=ysxGzsx
18 17 eqeq2d ⊢g=G→y+zsx=ysxgzsx↔y+zsx=ysxGzsx
19 18 anbi1d ⊢g=G→y+zsx=ysxgzsx∧y⁢zsx=yszsx↔y+zsx=ysxGzsx∧y⁢zsx=yszsx
20 19 ralbidv ⊢g=G→∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
21 16 20 anbi12d ⊢g=G→∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
22 21 ralbidv ⊢g=G→∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
23 22 anbi2d ⊢g=G→1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
24 6 23 raleqbidv ⊢g=G→∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
25 4 11 24 3anbi123d ⊢g=G→g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
26 feq1 ⊢s=S→s:ℂ×X⟶X↔S:ℂ×X⟶X
27 oveq ⊢s=S→1sx=1Sx
28 27 eqeq1d ⊢s=S→1sx=x↔1Sx=x
29 oveq ⊢s=S→ysxGz=ySxGz
30 oveq ⊢s=S→ysx=ySx
31 oveq ⊢s=S→ysz=ySz
32 30 31 oveq12d ⊢s=S→ysxGysz=ySxGySz
33 29 32 eqeq12d ⊢s=S→ysxGz=ysxGysz↔ySxGz=ySxGySz
34 33 ralbidv ⊢s=S→∀z∈XysxGz=ysxGysz↔∀z∈XySxGz=ySxGySz
35 oveq ⊢s=S→y+zsx=y+zSx
36 oveq ⊢s=S→zsx=zSx
37 30 36 oveq12d ⊢s=S→ysxGzsx=ySxGzSx
38 35 37 eqeq12d ⊢s=S→y+zsx=ysxGzsx↔y+zSx=ySxGzSx
39 oveq ⊢s=S→y⁢zsx=y⁢zSx
40 oveq ⊢s=S→yszsx=ySzsx
41 36 oveq2d ⊢s=S→ySzsx=ySzSx
42 40 41 eqtrd ⊢s=S→yszsx=ySzSx
43 39 42 eqeq12d ⊢s=S→y⁢zsx=yszsx↔y⁢zSx=ySzSx
44 38 43 anbi12d ⊢s=S→y+zsx=ysxGzsx∧y⁢zsx=yszsx↔y+zSx=ySxGzSx∧y⁢zSx=ySzSx
45 44 ralbidv ⊢s=S→∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
46 34 45 anbi12d ⊢s=S→∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
47 46 ralbidv ⊢s=S→∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
48 28 47 anbi12d ⊢s=S→1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
49 48 ralbidv ⊢s=S→∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
50 26 49 3anbi23d ⊢s=S→G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
51 25 50 opelopabg ⊢G∈V∧S∈V→GS∈gs|g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
52 3 51 bitrid ⊢G∈V∧S∈V→GS∈CVecOLD↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx